English
There is a noncomputable equivalence between the center of SL(n,R) and the group of roots of unity in R, of order max(card n, 1).
Русский
Существует невычислимое эквивалентность между центром SL(n,R) и группой корней единицы в R порядка max(card n, 1).
LaTeX
$$center(SpecialLinearGroup n R) ≃* rootsOfUnity (max(card n, 1)) R$$
Lean4
/-- An equivalence of groups, from the center of the special linear group to the roots of unity.
See also `center_equiv_rootsOfUnity'`. -/
noncomputable def center_equiv_rootsOfUnity :
center (SpecialLinearGroup n R) ≃* rootsOfUnity (max (Fintype.card n) 1) R :=
(isEmpty_or_nonempty n).by_cases
(fun hn ↦
by
rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one, rootsOfUnity_one]
exact MulEquiv.ofUnique)
(fun _ ↦
(max_eq_left (NeZero.one_le : 1 ≤ Fintype.card n)).symm ▸ center_equiv_rootsOfUnity' (Classical.arbitrary n))
