Commit 2024-02-19 15:34 e478d1c0

View on Github →

feat(LinearAlgebra/Matrix): center of special linear group (#7826) The center of a special linear group of degree n is a subgroup composed of scalar matrices, in which the scalars are the n-th roots of 1.

Estimated changes

Modified Mathlib/Data/PNat/Defs.lean

added theorem Nat.toPNat'_zero

Modified Mathlib/GroupTheory/GroupAction/Units.lean

added theorem Units.smul_mk_apply

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added theorem Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton

added def Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'

added theorem Matrix.SpecialLinearGroup.mem_center_iff

added theorem Matrix.SpecialLinearGroup.scalar_eq_coe_self_center

added theorem Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem rootsOfUnity_one