Basis

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

Statistics

Metric	Count
Definitions basis, equivRootSystem	2
Theorems basis_A_eq, instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'	2
Total	4

RootPairing.GeckConstruction

Definitions

Name	Category	Theorems
basis 📖	CompOp	1 math math: basis_A_eq
equivRootSystem 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_A_eq 📖	mathematical	—	LieAlgebra.Basis.A Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra Finite.of_fintype instIsDomain Field.toSemifield Subtype.finite LieSubalgebra.lieRing LieSubalgebra.lieAlgebra basis RootPairing.Base.cartanMatrix	—	Finite.of_fintype instIsDomain Subtype.finite
instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra' 📖	mathematical	—	LieSubalgebra.IsCartanSubalgebra Matrix Finset SetLike.instMembership Finset.instSetLike RootPairing.Base.support EuclideanDomain.toCommRing Field.toEuclideanDomain LieSubalgebra LieRing.ofAssociativeRing Matrix.instRing instFintypeSum Finset.Subtype.fintype CommRing.toRing LieAlgebra.ofAssociativeAlgebra Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id LieSubalgebra.instSetLike lieAlgebra Finite.of_fintype instIsDomain Field.toSemifield LieSubalgebra.lieRing LieSubalgebra.lieAlgebra cartanSubalgebra'	—	—

---

← Back to Index