Classical

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

Statistics

Metric	Count
Definitions JB, JD, PB, PD, Pso, S, indefiniteDiagonal, invertiblePB, invertiblePD, invertiblePso, so, so', soIndefiniteEquiv, typeB, typeBEquivSo', typeD, typeDEquivSo', single, singleSubSingle, sl, sp	21
Theorems indefiniteDiagonal_assoc, indefiniteDiagonal_transform, jb_transform, jd_transform, mem_so, pb_inv, pd_inv, pso_inv, s_as_blocks, soIndefiniteEquiv_apply, singleSubSingle_add_singleSubSingle, singleSubSingle_sub_singleSubSingle, singleSubSingle_sub_singleSubSingle', sl_bracket, sl_non_abelian, val_single, val_singleSubSingle, matrix_trace_commutator_zero	18
Total	39

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_trace_commutator_zero 📖	mathematical	—	Matrix.trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Bracket.bracket Matrix LieRingModule.toBracket LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieRing.toAddCommGroup lieRingSelfModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.trace_sub Matrix.trace_mul_comm sub_self

LieAlgebra.Orthogonal

Definitions

Name	Category	Theorems
JB 📖	CompOp	1 math math: jb_transform
JD 📖	CompOp	1 math math: jd_transform
PB 📖	CompOp	2 math math: jb_transform, pb_inv
PD 📖	CompOp	3 math math: jd_transform, pb_inv, pd_inv
Pso 📖	CompOp	3 math math: soIndefiniteEquiv_apply, pso_inv, indefiniteDiagonal_transform
S 📖	CompOp	3 math math: jb_transform, s_as_blocks, jd_transform
indefiniteDiagonal 📖	CompOp	2 math math: indefiniteDiagonal_assoc, indefiniteDiagonal_transform
invertiblePB 📖	CompOp	—
invertiblePD 📖	CompOp	1 math math: pb_inv
invertiblePso 📖	CompOp	—
so 📖	CompOp	2 math math: mem_so, soIndefiniteEquiv_apply
so' 📖	CompOp	1 math math: soIndefiniteEquiv_apply
soIndefiniteEquiv 📖	CompOp	1 math math: soIndefiniteEquiv_apply
typeB 📖	CompOp	—
typeBEquivSo' 📖	CompOp	—
typeD 📖	CompOp	—
typeDEquivSo' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indefiniteDiagonal_assoc 📖	mathematical	—	indefiniteDiagonal DFunLike.coe LieEquiv Matrix LieRing.ofAssociativeRing Matrix.instRing instFintypeSum PUnit.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id EquivLike.toFunLike LieEquiv.instEquivLike Matrix.reindexLieEquiv Equiv.symm Equiv.sumAssoc Matrix.fromBlocks Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Matrix.zero	—	Matrix.ext Matrix.one_apply_eq Sum.inl_injective Sum.inr_injective
indefiniteDiagonal_transform 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose Pso indefiniteDiagonal Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.ext Matrix.diagonal_transpose Matrix.diagonal_mul_diagonal Matrix.mul_diagonal Matrix.diagonal_apply_eq mul_one Matrix.diagonal_apply_ne Matrix.one_apply_ne MulZeroClass.zero_mul mul_neg neg_mul neg_neg
jb_transform 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose PB JB Matrix.smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat Matrix.fromBlocks Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne Matrix.zero S	—	Nat.instAtLeastTwoHAddOfNat Matrix.fromBlocks_transpose Matrix.transpose_one Matrix.fromBlocks_multiply Algebra.mul_smul_comm mul_one Matrix.mul_zero add_zero Matrix.zero_mul Matrix.mul_smul Algebra.to_smulCommClass Matrix.mul_one smul_zero zero_add jd_transform Matrix.fromBlocks_smul
jd_transform 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.transpose PD JD Matrix.smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat S	—	Matrix.fromBlocks_transpose Matrix.transpose_one Matrix.transpose_neg Matrix.fromBlocks_multiply MulZeroClass.mul_zero mul_one zero_add add_zero Nat.instAtLeastTwoHAddOfNat PD.eq_1 s_as_blocks Matrix.fromBlocks_smul mul_neg neg_add_cancel add_neg_cancel two_smul smul_zero smul_neg neg_add_rev
mem_so 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike so Matrix.transpose Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup	—	so.eq_1 mem_skewAdjointMatricesLieSubalgebra mem_skewAdjointMatricesSubmodule Matrix.mul_one Matrix.one_mul
pb_inv 📖	mathematical	—	Matrix Matrix.instMulOfFintypeOfAddCommMonoid instFintypeSum PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid PB Matrix.fromBlocks Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.zero Invertible.invOf PD invertiblePD	—	Nat.instAtLeastTwoHAddOfNat PB.eq_1 Matrix.fromBlocks_multiply mul_invOf_self Matrix.mul_one Matrix.mul_zero add_zero Matrix.zero_mul zero_add Matrix.fromBlocks_one
pd_inv 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid PD Matrix.smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Invertible.invOf AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat Matrix.transpose Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Nat.instAtLeastTwoHAddOfNat PD.eq_1 Matrix.fromBlocks_transpose Matrix.fromBlocks_smul Matrix.fromBlocks_multiply Matrix.transpose_one Algebra.mul_smul_comm mul_one Matrix.transpose_neg smul_neg mul_neg neg_neg invOf_two_smul_add_invOf_two_smul add_neg_cancel Matrix.fromBlocks_one
pso_inv 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum NonUnitalNonAssocSemiring.toAddCommMonoid Pso Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.ext Matrix.mul_diagonal Matrix.diagonal_apply_eq mul_one Matrix.diagonal_apply_ne Matrix.one_apply_ne mul_neg MulZeroClass.zero_mul neg_zero neg_neg
s_as_blocks 📖	mathematical	—	S Matrix.fromBlocks Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.zero Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing	—	Matrix.diagonal_one Matrix.diagonal_neg Matrix.fromBlocks_diagonal
soIndefiniteEquiv_apply 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid LieRing.toAddCommGroup LieRing.ofAssociativeRing CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Matrix LieSubalgebra Matrix.instRing instFintypeSum LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike so DFunLike.coe LieEquiv so' LieSubalgebra.lieRing LieSubalgebra.lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike soIndefiniteEquiv Matrix.instHMulOfFintypeOfMulOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.inv Pso	—	soIndefiniteEquiv.eq_1 LieEquiv.trans_apply LieEquiv.ofEq_apply

LieAlgebra.SpecialLinear

Definitions

Name	Category	Theorems
single 📖	CompOp	1 math math: val_single
singleSubSingle 📖	CompOp	4 math math: singleSubSingle_add_singleSubSingle, singleSubSingle_sub_singleSubSingle, val_singleSubSingle, singleSubSingle_sub_singleSubSingle'
sl 📖	CompOp	7 math math: singleSubSingle_add_singleSubSingle, sl_bracket, val_single, singleSubSingle_sub_singleSubSingle, val_singleSubSingle, singleSubSingle_sub_singleSubSingle', sl_non_abelian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singleSubSingle_add_singleSubSingle 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddMemClass.toAddCommSemigroup Matrix.addCommSemigroup AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddSubmonoidClass.toAddMemClass Matrix.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddSubgroupClass.toAddSubmonoidClass AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup LieSubalgebra.instAddSubgroupClass DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieAlgebra.toModule LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LinearMap.instFunLike singleSubSingle	—	AddSubmonoidClass.toAddMemClass AddSubgroupClass.toAddSubmonoidClass LieSubalgebra.instAddSubgroupClass Matrix.isScalarTower IsScalarTower.right sub_add_sub_cancel
singleSubSingle_sub_singleSubSingle 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl AddSubgroupClass.sub AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne LieSubalgebra.instAddSubgroupClass DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieAlgebra.toModule LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LinearMap.instFunLike singleSubSingle	—	LieSubalgebra.instAddSubgroupClass Matrix.isScalarTower IsScalarTower.right sub_sub_sub_cancel_left
singleSubSingle_sub_singleSubSingle' 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl AddSubgroupClass.sub AddGroup.toSubNegMonoid Matrix.addGroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne LieSubalgebra.instAddSubgroupClass DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieAlgebra.toModule LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LinearMap.instFunLike singleSubSingle	—	LieSubalgebra.instAddSubgroupClass Matrix.isScalarTower IsScalarTower.right sub_sub_sub_cancel_right
sl_bracket 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl Bracket.bracket LieRingModule.toBracket LieSubalgebra.lieRing LieRing.toAddCommGroup lieRingSelfModule Matrix.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	—
sl_non_abelian 📖	mathematical	Fintype.card	IsLieAbelian Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl 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 Fintype.exists_pair_of_one_lt_card Matrix.isScalarTower IsScalarTower.right sub_eq_zero sl_bracket LieModule.IsTrivial.trivial ZeroMemClass.coe_zero Finset.sum_congr mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq Finset.sum_const_zero NeZero.one
val_single 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieAlgebra.toModule LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LinearMap.instFunLike single Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.isScalarTower IsScalarTower.right
val_singleSubSingle 📖	mathematical	—	Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id SetLike.instMembership LieSubalgebra.instSetLike sl DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieSubalgebra.lieRing LieAlgebra.toModule LieSubalgebra.instModuleSubtypeMemOfIsScalarTower Algebra.toSMul Matrix.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.right LinearMap.instFunLike singleSubSingle Matrix.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.isScalarTower IsScalarTower.right

LieAlgebra.Symplectic

Definitions

Name	Category	Theorems
sp 📖	CompOp	—

---

← Back to Index