Commit 2025-11-30 21:13 addb2cac

View on Github →

feat:(LinearAlgebra/SpecialLinearGroup) : center of the special linear group of a module (#31078) prove that the center special linear group of a module consists with roots of unity compare with the corresponding result Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

deleted theorem rank_pos_of_free

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

added theorem Module.finrank_eq_zero_iff_of_free

added theorem Module.finrank_pos_iff_of_free

added theorem Module.rank_pos_iff_of_free

added theorem Module.rank_pos_of_free

added theorem Module.rank_zero_iff_of_free

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Matrix.toLin_scalar

Modified Mathlib/LinearAlgebra/SpecialLinearGroup.lean

modified def Matrix.SpecialLinearGroup.toLin'_equiv

added theorem Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq

added theorem Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq

added theorem SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq

added theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply

added theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply

added theorem SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one

added theorem SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply

added theorem SpecialLinearGroup.center_eq_bot_of_finrank_le_one

added theorem SpecialLinearGroup.mem_center_iff

added theorem SpecialLinearGroup.mem_center_iff_spec

added theorem rootsOfUnity.eq_one