Commit 2025-11-16 15:54 984810dd

View on Github →

feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module (#30987) Define the special linear group of a module. Relate it with Matrix.SpecialLinearGroup. Several additional constructions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Charpoly/BaseChange.lean

added theorem LinearEquiv.det_baseChange

modified theorem LinearMap.charpoly_baseChange

modified theorem LinearMap.det_baseChange

modified theorem LinearMap.det_eq_sign_charpoly_coeff

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem LinearMap.coe_equivOfIsUnitDet

added theorem LinearMap.det_dualMap

added theorem LinearMap.equivOfIsUnitDet_apply

Modified Mathlib/LinearAlgebra/Dimension/Free.lean

added theorem LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one

added theorem Module.Basis.nonempty_unique_index_of_finrank_eq_one

added theorem Module.nonempty_linearEquiv_of_finrank_eq_one

Modified Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

Modified Mathlib/LinearAlgebra/GeneralLinearGroup.lean

added theorem LinearMap.GeneralLinearGroup.ofLinearEquiv_inv

added theorem LinearMap.GeneralLinearGroup.ofLinearEquiv_mul

added theorem LinearMap.GeneralLinearGroup.toLinearEquiv_inv

added theorem LinearMap.GeneralLinearGroup.toLinearEquiv_mul

Modified Mathlib/LinearAlgebra/Matrix/Dual.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

added theorem Matrix.GeneralLinearGroup.toLin'_apply

Created Mathlib/LinearAlgebra/SpecialLinearGroup.lean

added def Matrix.SpecialLinearGroup.toLin'_equiv

added def SpecialLinearGroup.baseChange

added theorem SpecialLinearGroup.coe_div

added theorem SpecialLinearGroup.coe_dualMap

added theorem SpecialLinearGroup.coe_inv

added theorem SpecialLinearGroup.coe_mk

added theorem SpecialLinearGroup.coe_mul

added theorem SpecialLinearGroup.coe_one

added theorem SpecialLinearGroup.coe_pow

added theorem SpecialLinearGroup.coe_toGeneralLinearGroup_apply

added theorem SpecialLinearGroup.coe_zpow

added def SpecialLinearGroup.congr_linearEquiv

added theorem SpecialLinearGroup.congr_linearEquiv_apply_apply

added theorem SpecialLinearGroup.congr_linearEquiv_coe_apply

added theorem SpecialLinearGroup.congr_linearEquiv_refl

added theorem SpecialLinearGroup.congr_linearEquiv_symm

added theorem SpecialLinearGroup.congr_linearEquiv_trans

added theorem SpecialLinearGroup.det_coe

added theorem SpecialLinearGroup.det_eq_one

added def SpecialLinearGroup.dualMap

added theorem SpecialLinearGroup.ext

added theorem SpecialLinearGroup.ext_iff

added theorem SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff

added theorem SpecialLinearGroup.subsingleton_of_finrank_eq_one

added def SpecialLinearGroup.toGeneralLinearGroup

added theorem SpecialLinearGroup.toGeneralLinearGroup_injective

added theorem SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply

added def SpecialLinearGroup.toLinearEquiv

added theorem SpecialLinearGroup.toLinearEquiv_apply

added theorem SpecialLinearGroup.toLinearEquiv_injective

added theorem SpecialLinearGroup.toLinearEquiv_symm_apply

added theorem SpecialLinearGroup.toLinearEquiv_symm_to_linearMap

added theorem SpecialLinearGroup.toLinearEquiv_to_linearMap

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem LinearEquiv.baseChange_inv

added theorem LinearEquiv.baseChange_mul

added theorem LinearEquiv.baseChange_one

added theorem LinearEquiv.baseChange_pow

added theorem LinearEquiv.baseChange_symm

added theorem LinearEquiv.baseChange_trans

added theorem LinearEquiv.baseChange_zpow

added theorem LinearEquiv.coe_baseChange