Commit 2026-07-22 17:55 b8a692e1

View on Github →

chore: split file Algebra.Lie.Algebra.Basis (#41985)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Basis/Base.lean

added def LieAlgebra.Basis.base

added def LieAlgebra.Basis.baseSupp'

added def LieAlgebra.Basis.baseSupportEquiv

added theorem LieAlgebra.Basis.cartanMatrix_base_eq

added theorem LieAlgebra.Basis.coe_baseSupportEquiv_apply

added theorem LieAlgebra.Basis.coe_linearMap_baseSupp'

added theorem LieAlgebra.Basis.coroot_eq_h'

added theorem LieAlgebra.Basis.linearIndepOn_root_baseSupp

added theorem LieAlgebra.Basis.root_mem_or_mem_neg

Renamed Mathlib/Algebra/Lie/Basis.lean to Mathlib/Algebra/Lie/Basis/Basic.lean

deleted def LieAlgebra.Basis.base

deleted def LieAlgebra.Basis.baseSupp'

deleted def LieAlgebra.Basis.baseSupportEquiv

deleted theorem LieAlgebra.Basis.cartanMatrix_base_eq

deleted theorem LieAlgebra.Basis.coe_baseSupportEquiv_apply

deleted theorem LieAlgebra.Basis.coe_linearMap_baseSupp'

deleted theorem LieAlgebra.Basis.coroot_eq_h'

deleted theorem LieAlgebra.Basis.linearIndepOn_root_baseSupp

deleted theorem LieAlgebra.Basis.root_mem_or_mem_neg

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basis.lean