Basic

📁 Source: Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

Statistics

Metric	Count
Definitions cartanSubalgebra, cartanSubalgebra', e, f, h, h', lieAlgebra, u, v, ω, ωConj, ωConjLieSubmodule	12
Theorems apply_inr_eq_zero_of_mem_span_range_u, apply_sum_inl_eq_zero_of_mem_span_h, cartanSubalgebra_eq_lieSpan, cartanSubalgebra_le_lieAlgebra, diagonal_elim_mem_span_h_iff, e_lie_u, e_lie_v_ne, e_mem_lieAlgebra, f_lie_v_ne, f_lie_v_same, f_mem_lieAlgebra, h_def, h_eq_diagonal, h_mem_cartanSubalgebra, h_mem_cartanSubalgebra', h_mem_lieAlgebra, instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, lie_e_f_mul_ω, lie_e_lie_f_apply, lie_h_h, mem_ωConjLieSubmodule_iff, span_range_h'_eq_top, span_range_h_le_range_diagonal, ωConjLieSubmodule_eq_top_iff, ωConj_invFun, ωConj_mem_of_mem, ωConj_toFun, ω_mul_e, ω_mul_f, ω_mul_h, ω_mul_ω	33
Total	45

RootPairing.GeckConstruction

Definitions

Name	Category	Theorems
cartanSubalgebra 📖	CompOp	4 math math: instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, h_mem_cartanSubalgebra, cartanSubalgebra_eq_lieSpan, cartanSubalgebra_le_lieAlgebra
cartanSubalgebra' 📖	CompOp	5 math math: span_range_h'_eq_top, instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, h_mem_cartanSubalgebra', coe_genWeightSpace_zero_eq_span_range_u
e 📖	CompOp	12 math math: isSl2Triple, lie_h_e, lie_e_f_same, e_lie_v_ne, ω_mul_e, isNilpotent_e, ω_mul_f, lie_e_lie_f_apply, e_mem_lieAlgebra, lie_e_f_mul_ω, e_lie_u, lie_e_f_ne
f 📖	CompOp	12 math math: isSl2Triple, isNilpotent_f, lie_e_f_same, f_lie_v_ne, ω_mul_e, lie_h_f, ω_mul_f, lie_e_lie_f_apply, f_lie_v_same, f_mem_lieAlgebra, lie_e_f_mul_ω, lie_e_f_ne
h 📖	CompOp	14 math math: h_def, isSl2Triple, h_mem_cartanSubalgebra, trace_h_eq_zero, cartanSubalgebra_eq_lieSpan, lie_h_e, span_range_h_le_range_diagonal, ω_mul_h, diagonal_elim_mem_span_h_iff, lie_e_f_same, h_mem_lieAlgebra, lie_h_f, lie_h_h, h_eq_diagonal
h' 📖	CompOp	1 math math: span_range_h'_eq_top
lieAlgebra 📖	CompOp	13 math math: instHasTrivialRadical, mem_ωConjLieSubmodule_iff, trace_toEnd_eq_zero, span_range_h'_eq_top, instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', instIsIrreducible, ωConjLieSubmodule_eq_top_iff, cartanSubalgebra_le_lieAlgebra, instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, h_mem_lieAlgebra, f_mem_lieAlgebra, e_mem_lieAlgebra, coe_genWeightSpace_zero_eq_span_range_u
u 📖	CompOp	4 math math: lie_e_lie_f_apply, f_lie_v_same, coe_genWeightSpace_zero_eq_span_range_u, e_lie_u
v 📖	CompOp	4 math math: f_lie_v_ne, e_lie_v_ne, f_lie_v_same, e_lie_u
ω 📖	CompOp	8 math math: mem_ωConjLieSubmodule_iff, ω_mul_h, ωConj_invFun, ω_mul_ω, ωConj_toFun, ω_mul_e, ω_mul_f, lie_e_f_mul_ω
ωConj 📖	CompOp	3 math math: ωConj_invFun, ωConj_toFun, ωConj_mem_of_mem
ωConjLieSubmodule 📖	CompOp	2 math math: mem_ωConjLieSubmodule_iff, ωConjLieSubmodule_eq_top_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_inr_eq_zero_of_mem_span_range_u 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Submodule.setLike Submodule.span Set.range u	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Submodule.span_induction Pi.single_eq_of_ne add_zero MulZeroClass.mul_zero
apply_sum_inl_eq_zero_of_mem_span_h 📖	mathematical	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Submodule CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Submodule.setLike Submodule.span Set.range h	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Submodule.span_induction add_zero MulZeroClass.mul_zero
cartanSubalgebra_eq_lieSpan 📖	mathematical	—	cartanSubalgebra LieSubalgebra.lieSpan Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id Set.range h	—	le_antisymm LieSubalgebra.submodule_span_le_lieSpan LieSubalgebra.lieSpan_le cartanSubalgebra.eq_1 Submodule.subset_span
cartanSubalgebra_le_lieAlgebra 📖	mathematical	—	LieSubalgebra Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id Preorder.toLE PartialOrder.toPreorder LieSubalgebra.instPartialOrder_1 cartanSubalgebra lieAlgebra	—	cartanSubalgebra.eq_1 lieAlgebra.eq_1 LieSubalgebra.toSubmodule_le_toSubmodule Submodule.span_le LieSubalgebra.subset_lieSpan Set.mem_range_self
diagonal_elim_mem_span_h_iff 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Submodule CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Submodule.setLike Submodule.span Set.range h Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instZero Pi.addCommMonoid Pi.Function.module AddGroupWithOne.toIntCast Ring.toAddGroupWithOne RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra	—	Matrix.ext add_zero MulZeroClass.mul_zero Matrix.diagonal_apply_ne Set.ext h_def Set.image_congr RingHomSurjective.ids Submodule.span_image Submodule.map.congr_simp RingHomCompTriple.ids
e_lie_u 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup Matrix.instLieRingModuleForall e u SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne abs instLatticeInt Int.instAddGroup RootPairing.Base.cartanMatrix v	—	Matrix.mulVec_single smul_zero Pi.single_eq_of_ne smul_ite one_smul Pi.single_apply zsmul_eq_mul mul_one
e_lie_v_ne 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support	Bracket.bracket Matrix LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup Matrix.instLieRingModuleForall e v Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RootPairing.chainBotCoeff AddMonoidWithOne.toOne	—	RootPairing.ne_zero CharZero.NeZero.two RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self add_neg_cancel Matrix.mulVec_single smul_zero Pi.single_eq_of_ne MulZeroClass.mul_zero Function.instEmbeddingLikeEmbedding smul_ite smul_add one_smul Pi.single_apply mul_ite mul_one
e_mem_lieAlgebra 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra e	—	LieSubalgebra.subset_lieSpan
f_lie_v_ne 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support	Bracket.bracket Matrix LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup Matrix.instLieRingModuleForall f v Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RootPairing.chainTopCoeff AddMonoidWithOne.toOne	—	RootPairing.ne_zero CharZero.NeZero.two AddRightCancelSemigroup.toIsRightCancelAdd Matrix.mulVec_single smul_zero Pi.single_eq_of_ne MulZeroClass.mul_zero add_sub_cancel_right Function.instEmbeddingLikeEmbedding smul_ite smul_add one_smul Pi.single_apply mul_ite mul_one
f_lie_v_same 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup Matrix.instLieRingModuleForall f v u	—	Matrix.mulVec_single smul_ite one_smul smul_zero Pi.single_apply sub_self RootPairing.ne_zero CharZero.NeZero.two Pi.single_eq_of_ne
f_mem_lieAlgebra 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra f	—	LieSubalgebra.subset_lieSpan
h_def 📖	mathematical	—	h Matrix.fromBlocks Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.diagonal AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra	—	Matrix.ext
h_eq_diagonal 📖	mathematical	—	h Matrix.diagonal Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.instZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra	—	Matrix.ext Matrix.diagonal_apply_ne
h_mem_cartanSubalgebra 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike cartanSubalgebra h	—	Submodule.subset_span Set.mem_range_self
h_mem_cartanSubalgebra' 📖	mathematical	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra h	LieSubalgebra.lieRing LieSubalgebra.lieAlgebra cartanSubalgebra'	—	—
h_mem_lieAlgebra 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra h	—	LieSubalgebra.subset_lieSpan
instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra 📖	mathematical	—	IsLieAbelian Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike cartanSubalgebra LieRingModule.toBracket LieSubalgebra.lieRing LieRing.toAddCommGroup lieRingSelfModule ZeroMemClass.zero Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toZeroMemClass Matrix.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup LieSubalgebra.instAddSubgroupClass	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass cartanSubalgebra_eq_lieSpan LieSubalgebra.isLieAbelian_lieSpan_iff lie_h_h
instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra' 📖	mathematical	—	IsLieAbelian Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra LieSubalgebra.lieRing LieSubalgebra.lieAlgebra cartanSubalgebra' LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule ZeroMemClass.zero Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toZeroMemClass Matrix.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup LieSubalgebra.instAddSubgroupClass SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass trivial_lie_zero instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra
instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall 📖	mathematical	—	LieModule.IsTriangularizable Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra LieSubalgebra.lieRing LieSubalgebra.lieAlgebra cartanSubalgebra' Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule LieSubalgebra.lieRingModule Matrix.instLieRingModuleForall LieSubalgebra.lieModule Matrix.instLieModuleForall	—	LieSubalgebra.lieModule Matrix.instLieModuleForall smulCommClass_self IsScalarTower.left span_range_h_le_range_diagonal RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right LieModule.toEnd_matrix Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace Matrix.iSup_eigenspace_toLin'_diagonal_eq_top
lie_e_f_mul_ω 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Bracket.bracket Ring.instBracket Matrix.nonUnitalNonAssocRing e f ω Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing	—	Ring.lie_def sub_mul mul_assoc ω_mul_e ω_mul_f mul_sub neg_mul sub_neg_eq_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
lie_e_lie_f_apply 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup Matrix.instLieRingModuleForall e f u SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne abs instLatticeInt Int.instAddGroup RootPairing.Base.cartanMatrix	—	Matrix.mulVec_single one_smul Finset.sum_congr Fintype.sum_sum_type MulZeroClass.mul_zero Finset.sum_const_zero mul_ite ite_mul one_mul MulZeroClass.zero_mul Finset.sum_ite_eq' zero_add Pi.single_apply smul_ite zsmul_eq_mul mul_one smul_zero RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self add_neg_cancel Nat.instAtLeastTwoHAddOfNat RootPairing.ne_zero CharZero.NeZero.two add_zero Pi.single_eq_of_ne
lie_h_h 📖	mathematical	—	Bracket.bracket Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Ring.instBracket Matrix.nonUnitalNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instFintypeSum Finset.Subtype.fintype h Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	h_eq_diagonal Matrix.commute_diagonal
mem_ωConjLieSubmodule_iff 📖	mathematical	—	LieSubmodule Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra LieSubalgebra.lieRing Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule LieSubalgebra.lieRingModule Matrix.instLieRingModuleForall LieSubmodule.instSetLike ωConjLieSubmodule Matrix.mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ω	—	—
span_range_h'_eq_top 📖	mathematical	—	Submodule.span Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra LieSubalgebra.lieRing LieSubalgebra.lieAlgebra cartanSubalgebra' CommSemiring.toSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LieSubalgebra.instIsScalarTowerSubtypeMem Set.range h' Top.top Submodule Submodule.instTop	—	Matrix.isScalarTower IsScalarTower.right LieSubalgebra.instIsScalarTowerSubtypeMem eq_top_iff RingHomCompTriple.ids RingHomSurjective.ids Submodule.map_span Set.range_comp SetLike.mem_coe Function.Injective.mem_set_image Submodule.injective_subtype Set.image_comp
span_range_h_le_range_diagonal 📖	mathematical	—	Submodule Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support CommSemiring.toSemiring CommRing.toCommSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.span Set.range h LinearMap.range Pi.addCommMonoid Pi.Function.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Matrix.diagonalLinearMap	—	RingHomSurjective.ids Submodule.span_le h_eq_diagonal LinearMap.mem_range_self
ωConjLieSubmodule_eq_top_iff 📖	mathematical	—	ωConjLieSubmodule Top.top LieSubmodule Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra LieSubalgebra.lieRing Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule LieSubalgebra.lieRingModule Matrix.instLieRingModuleForall LieSubmodule.instTop	—	LieSubmodule.toSubmodule_eq_top RingHomSurjective.ids RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Function.Involutive.bijective Matrix.mulVec_mulVec ω_mul_ω Matrix.one_mulVec OrderIso.instOrderIsoClass
ωConj_invFun 📖	mathematical	—	LieEquiv.invFun Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id ωConj Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω	—	—
ωConj_mem_of_mem 📖	mathematical	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra	DFunLike.coe LieEquiv EquivLike.toFunLike LieEquiv.instEquivLike ωConj	—	LieSubalgebra.lieSpan_induction neg_mem_iff AddSubgroupClass.toNegMemClass LieSubalgebra.instAddSubgroupClass LieSubalgebra.subset_lieSpan ω_mul_h neg_mul mul_assoc ω_mul_ω mul_one neg_neg ω_mul_e ω_mul_f MulZeroClass.mul_zero MulZeroClass.zero_mul AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass RingHomInvPair.ids LieEquiv.instLinearEquivClass SMulMemClass.smul_mem LieSubalgebra.instSMulMemClass LieEquiv.map_lie LieSubalgebra.lie_mem
ωConj_toFun 📖	mathematical	—	DFunLike.coe LieEquiv Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id EquivLike.toFunLike LieEquiv.instEquivLike ωConj Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω	—	—
ω_mul_e 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω e f	—	Matrix.ext Fintype.sum_sum_type Finset.sum_congr MulZeroClass.mul_zero Finset.sum_const_zero mul_ite MulZeroClass.zero_mul add_zero mul_one Finset.sum_ite_eq' Finset.sum_eq_single_of_mem Finset.mem_univ zero_add ite_mul one_mul neg_eq_iff_eq_neg RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self neg_add_rev sub_eq_add_neg RootPairing.chainTopCoeff_reflectionPerm_right
ω_mul_f 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω f e	—	ω_mul_e mul_assoc ω_mul_ω mul_one one_mul
ω_mul_h 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω h Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing	—	Matrix.ext Fintype.sum_sum_type Finset.sum_congr MulZeroClass.mul_zero Finset.sum_const_zero add_zero neg_mul Finset.sum_neg_distrib mul_ite mul_one neg_zero MulZeroClass.zero_mul RootPairing.pairingIn.congr_simp ite_mul one_mul Finset.sum_ite_eq' zero_add RootPairing.pairingIn_reflectionPerm_self_left instFaithfulSMulIntOfCharZero Int.cast_neg neg_neg
ω_mul_ω 📖	mathematical	—	Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Finset.Subtype.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid ω Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.ext Fintype.sum_sum_type Finset.sum_congr mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq' Finset.sum_const_zero add_zero Matrix.one_apply_ne neg_neg zero_add

---

← Back to Index