BaseChange

📁 Source: Mathlib/Algebra/Lie/BaseChange.lean

Statistics

Metric	Count
Definitions instBaseLieAlgebra, instBracketTensorProduct, instLieAlgebra, instLieRing, instLieRingModule, map, instLieRingRestrictScalars, lieAlgebra, baseChange	9
Theorems bracket_tmul, instLieModule, map_apply_tmul, toEnd_baseChange, baseChange_bot, baseChange_top, coe_baseChange, lie_baseChange, mem_baseChange_iff, tmul_mem_baseChange_of_mem	10
Total	19

LieAlgebra.ExtendScalars

Definitions

Name	Category	Theorems
instBaseLieAlgebra 📖	CompOp	3 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, map_apply_tmul
instBracketTensorProduct 📖	CompOp	1 math math: bracket_tmul
instLieAlgebra 📖	CompOp	6 math math: LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieSubmodule.lie_baseChange, LieAlgebra.derivedSeries_baseChange, LieModule.toEnd_baseChange, LieAlgebra.derivedSeriesOfIdeal_baseChange, instLieModule
instLieRing 📖	CompOp	17 math math: LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, LieAlgebra.instIsSolvableTensorProduct, LieSubmodule.mem_baseChange_iff, LieModule.instIsNilpotentTensor, LieSubmodule.lie_baseChange, LieAlgebra.derivedSeries_baseChange, LieSubmodule.tmul_mem_baseChange_of_mem, LieModule.toEnd_baseChange, LieAlgebra.derivedSeriesOfIdeal_baseChange, instLieModule, LieAlgebra.isSolvable_tensorProduct_iff, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, LieSubmodule.coe_baseChange, LieSubmodule.baseChange_top, map_apply_tmul, LieSubmodule.baseChange_bot
instLieRingModule 📖	CompOp	10 math math: LieSubmodule.lowerCentralSeries_tensor_eq_baseChange, LieSubmodule.mem_baseChange_iff, LieModule.instIsNilpotentTensor, LieSubmodule.lie_baseChange, LieSubmodule.tmul_mem_baseChange_of_mem, LieModule.toEnd_baseChange, instLieModule, LieSubmodule.coe_baseChange, LieSubmodule.baseChange_top, LieSubmodule.baseChange_bot
map 📖	CompOp	1 math math: map_apply_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bracket_tmul 📖	mathematical	—	Bracket.bracket TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instBracketTensorProduct TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LieRingModule.toBracket	—	—
instLieModule 📖	mathematical	—	LieModule TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instLieRing instLieAlgebra TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass instLieRingModule	—	Algebra.to_smulCommClass TensorProduct.smulCommClass_left map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
map_apply_tmul 📖	mathematical	—	DFunLike.coe LieHom TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instLieRing instBaseLieAlgebra LieHom.instFunLike map TensorProduct.tmul AlgHom CommSemiring.toSemiring AlgHom.funLike	—	—

LieAlgebra.RestrictScalars

Definitions

Name	Category	Theorems
instLieRingRestrictScalars 📖	CompOp	—
lieAlgebra 📖	CompOp	—

LieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toEnd_baseChange 📖	mathematical	—	DFunLike.coe LieHom TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Module.End CommSemiring.toSemiring TensorProduct.addCommGroup TensorProduct.leftModule Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRing LieAlgebra.ExtendScalars.instLieAlgebra Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd LieAlgebra.ExtendScalars.instLieRingModule LieAlgebra.ExtendScalars.instLieModule TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne LinearMap.baseChange	—	TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.right Algebra.to_smulCommClass TensorProduct.isScalarTower_left smulCommClass_self IsScalarTower.left LieAlgebra.ExtendScalars.instLieModule LinearMap.ext_ring IsScalarTower.to_smulCommClass LinearMap.ext mul_one

LieSubmodule

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	9 math math: lowerCentralSeries_tensor_eq_baseChange, mem_baseChange_iff, lie_baseChange, LieAlgebra.derivedSeries_baseChange, tmul_mem_baseChange_of_mem, LieAlgebra.derivedSeriesOfIdeal_baseChange, coe_baseChange, baseChange_top, baseChange_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_bot 📖	mathematical	—	baseChange Bot.bot LieSubmodule instBot TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule	—	Algebra.to_smulCommClass Submodule.baseChange_bot
baseChange_top 📖	mathematical	—	baseChange Top.top LieSubmodule instTop TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule	—	Algebra.to_smulCommClass Submodule.baseChange_top
coe_baseChange 📖	mathematical	—	toSubmodule TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule baseChange Submodule.baseChange	—	Algebra.to_smulCommClass
lie_baseChange 📖	mathematical	—	baseChange Bracket.bracket LieIdeal LieSubmodule hasBracket TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule lieRingSelfModule lieAlgebraSelfModule LieAlgebra.ExtendScalars.instLieAlgebra	—	TensorProduct.smulCommClass_left smulCommClass_self Set.ext Set.image_congr Algebra.to_smulCommClass lieAlgebraSelfModule coe_baseChange lieIdeal_oper_eq_linear_span' Submodule.baseChange_span LieAlgebra.ExtendScalars.instLieModule le_antisymm Submodule.span_mono tmul_mem_baseChange_of_mem mul_one Submodule.span_le Submodule.span_induction₂ RingHomSurjective.ids Submodule.subset_span ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass zero_lie lie_zero add_lie AddSubmonoidClass.toAddMemClass lie_add smul_lie lie_smul mem_baseChange_iff
mem_baseChange_iff 📖	mathematical	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieSubmodule LieRing.toAddCommGroup LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule SetLike.instMembership instSetLike baseChange Submodule TensorProduct.addCommMonoid Submodule.setLike Submodule.span SetLike.coe TensorProduct.instModule Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid LinearMap.instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne toSubmodule	—	Algebra.to_smulCommClass RingHomSurjective.ids TensorProduct.smulCommClass_left smulCommClass_self Submodule.baseChange_eq_span
tmul_mem_baseChange_of_mem 📖	mathematical	LieSubmodule SetLike.instMembership instSetLike	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra LieRing.toAddCommGroup LieAlgebra.ExtendScalars.instLieRing TensorProduct.addCommGroup TensorProduct.leftModule CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass LieAlgebra.ExtendScalars.instLieRingModule baseChange TensorProduct.tmul	—	Submodule.tmul_mem_baseChange_of_mem

---

← Back to Index