Commit 2026-03-13 08:20 5dec42f0

View on Github →

feat: supporting lemmas for theory of bases in Lie theory (#36297) Split out from other work to simplify review.

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.inv_range'

Modified Mathlib/Algebra/Lie/Subalgebra.lean

added theorem LieSubalgebra.disjoint_toSubmodule

added theorem LieSubalgebra.lieSpan_neg

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.mem_sup_left

added theorem LieSubmodule.mem_sup_right

Modified Mathlib/Algebra/Lie/TraceForm.lean

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

added theorem LieAlgebra.eq_rootSpace_zero_iff_isCartan

added theorem LieAlgebra.mem_biSup_genWeightSpace_of

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

added theorem LieAlgebra.IsKilling.eq_coroot_of_mem_corootSpace_of_two

added theorem LieSubalgebra.isNonZero_coe_root

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

added theorem LinearMap.coe_zero_iff

Modified Mathlib/Data/Set/Finite/Range.lean

added theorem Set.Finite.exists_subset_finite_image_eq

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Module.Basis.linearIndependent_coord

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndependent.neg

added theorem linearIndependent_neg_iff

Modified Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

added theorem LinearIndependent.sum_smul_of_nondegenerate

Modified Mathlib/Order/CompactlyGenerated/Basic.lean

added theorem disjoint_biSup_of_finite_disjoint_biSup

added theorem iSupIndep.disjoint_biSup_biSup

Modified Mathlib/Order/ModularLattice.lean

added theorem disjoint_sup_right_of_disjoint_sup_right

added theorem le_iff_eq_of_codisjoint_of_disjoint

Modified Mathlib/Order/SupIndep.lean

added theorem iSupIndep.disjoint_biSup_biSup'

added theorem iSupIndep.le_iff_eq_of_iSup_eq_top

added theorem iSupIndep.mem_of_biSup_eq_top

added theorem iSupIndep_fin_three

added theorem iSup_fin_three

Modified Mathlib/RingTheory/Regular/Category.lean