English
Membership in the center is equivalent to the existence of a scalar r with r^{card(n)} = 1 and A = scalar n r.
Русский
Принадлежность центру эквивалентна существованию скаляра r, такого что r^{|n|}=1 и A = scalar n r.
LaTeX
$$A ∈ center(SL_n(R)) ⇔ ∃ r, r^{card(n)} = 1 ∧ scalar n r = A.val$$
Lean4
/-- The center of a special linear group of degree `n` is the subgroup of scalar matrices, for which
the scalars are the `n`-th roots of unity. -/
theorem mem_center_iff {A : SpecialLinearGroup n R} :
A ∈ center (SpecialLinearGroup n R) ↔ ∃ (r : R), r ^ (Fintype.card n) = 1 ∧ scalar n r = A :=
by
rcases isEmpty_or_nonempty n with hn | ⟨⟨i⟩⟩; · exact ⟨by aesop, by simp [Subsingleton.elim A 1]⟩
refine ⟨fun h ↦ ⟨A i i, ?_, ?_⟩, fun ⟨r, _, hr⟩ ↦ Subgroup.mem_center_iff.mpr fun B ↦ ?_⟩
· have : det ((scalar n) (A i i)) = 1 := (scalar_eq_self_of_mem_center h i).symm ▸ A.property
simpa using this
· exact scalar_eq_self_of_mem_center h i
· suffices ↑ₘ(B * A) = ↑ₘ(A * B) from Subtype.val_injective this
simpa only [coe_mul, ← hr] using (scalar_commute (n := n) r (Commute.all r) B).symm
