Matrix

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

Statistics

Metric	Count
Definitions instLieRingModuleForall, lieConj, reindexLieEquiv, lieEquivMatrix'	4
Theorems instIsFaithfulMatrixForall, toEnd_matrix, instLieModuleForall, lieConj_apply, lieConj_symm_apply, lie_apply, reindexLieEquiv_apply, reindexLieEquiv_symm, lieEquivMatrix'_apply, lieEquivMatrix'_symm_apply	10
Total	14

LieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsFaithfulMatrixForall 📖	mathematical	—	IsFaithful Matrix LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule Matrix.instLieRingModuleForall Matrix.instLieModuleForall	—	Matrix.instLieModuleForall smulCommClass_self IsScalarTower.left Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right toEnd_matrix EmbeddingLike.injective EquivLike.toEmbeddingLike
toEnd_matrix 📖	mathematical	—	toEnd Matrix LieRing.ofAssociativeRing Matrix.instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule Matrix.instLieRingModuleForall Matrix.instLieModuleForall LieEquiv.toLieHom Module.End Pi.addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.End.instRing Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right LieEquiv.symm lieEquivMatrix'	—	LieHom.ext smulCommClass_self IsScalarTower.left Matrix.instLieModuleForall Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right LinearMap.pi_ext' Finite.of_fintype LinearMap.ext_ring RingHomCompTriple.ids Matrix.mulVec_single one_smul

Matrix

Definitions

Name	Category	Theorems
instLieRingModuleForall 📖	CompOp	15 math math: LieModule.instIsFaithfulMatrixForall, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, RootPairing.GeckConstruction.trace_toEnd_eq_zero, instLieModuleForall, RootPairing.GeckConstruction.instIsIrreducible, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, lie_apply, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.f_lie_v_ne, RootPairing.GeckConstruction.e_lie_v_ne, RootPairing.GeckConstruction.lie_e_lie_f_apply, RootPairing.GeckConstruction.f_lie_v_same, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, RootPairing.GeckConstruction.e_lie_u, LieModule.toEnd_matrix
lieConj 📖	CompOp	2 math math: lieConj_apply, lieConj_symm_apply
reindexLieEquiv 📖	CompOp	3 math math: LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, reindexLieEquiv_apply, reindexLieEquiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLieModuleForall 📖	mathematical	—	LieModule Matrix LieRing.ofAssociativeRing instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id Pi.addCommGroup LieRing.toAddCommGroup Pi.Function.module CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LieAlgebra.toModule instLieRingModuleForall	—	smul_mulVec IsScalarTower.right mulVec_smul Algebra.to_smulCommClass
lieConj_apply 📖	mathematical	—	DFunLike.coe LieEquiv Matrix LieRing.ofAssociativeRing instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id EquivLike.toFunLike LieEquiv.instEquivLike lieConj instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	RingHomInvPair.triples₂ RingHomInvPair.ids RingHomCompTriple.ids Function.smulCommClass Algebra.to_smulCommClass LinearMap.comp.congr_simp invOf_eq_nonsing_inv LinearMap.toMatrix'_comp LinearMap.toMatrix'_toLin'
lieConj_symm_apply 📖	mathematical	—	DFunLike.coe LieEquiv Matrix LieRing.ofAssociativeRing instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm lieConj instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass RingHomInvPair.triples₂ RingHomCompTriple.ids LinearMap.comp.congr_simp invOf_eq_nonsing_inv LinearMap.toMatrix'_comp LinearMap.toMatrix'_toLin'
lie_apply 📖	mathematical	—	Bracket.bracket Matrix LieRingModule.toBracket LieRing.ofAssociativeRing instRing CommRing.toRing Pi.addCommGroup LieRing.toAddCommGroup instLieRingModuleForall mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
reindexLieEquiv_apply 📖	mathematical	—	DFunLike.coe LieEquiv Matrix LieRing.ofAssociativeRing instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id EquivLike.toFunLike LieEquiv.instEquivLike reindexLieEquiv Equiv Equiv.instEquivLike reindex	—	—
reindexLieEquiv_symm 📖	mathematical	—	LieEquiv.symm Matrix LieRing.ofAssociativeRing instRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id reindexLieEquiv Equiv.symm	—	—

(root)

Definitions

Name	Category	Theorems
lieEquivMatrix' 📖	CompOp	3 math math: lieEquivMatrix'_apply, lieEquivMatrix'_symm_apply, LieModule.toEnd_matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieEquivMatrix'_apply 📖	mathematical	—	DFunLike.coe LieEquiv Module.End CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Matrix Module.End.instRing Pi.addCommGroup LieRing.toAddCommGroup Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instRing Matrix.instAlgebra Ring.toSemiring EquivLike.toFunLike LieEquiv.instEquivLike lieEquivMatrix' LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module Matrix.module DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix'	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
lieEquivMatrix'_symm_apply 📖	mathematical	—	DFunLike.coe LieEquiv Matrix Module.End CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module LieAlgebra.toModule LieRing.ofAssociativeRing CommRing.toRing LieAlgebra.ofAssociativeAlgebra Algebra.id Matrix.instRing Matrix.instAlgebra Ring.toSemiring Module.End.instRing Pi.addCommGroup LieRing.toAddCommGroup Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right EquivLike.toFunLike LieEquiv.instEquivLike LieEquiv.symm lieEquivMatrix' LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module DFinsupp.instEquivLikeLinearEquiv Matrix.toLin'	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right

---

← Back to Index