English
Cyclotomic extensions are abelian; the automorphisms over the base commute.
Русский
Циклотомические расширения абелизованы; автоморфизмы над базой commute.
LaTeX
$$$[IsCyclotomicExtension S A B]\\Rightarrow IsMulCommutative( B \\simeq_A B )$$$
Lean4
/-- Cyclotomic extensions are abelian. -/
theorem isMulCommutative [IsCyclotomicExtension S A B] [IsDomain B] : IsMulCommutative (B ≃ₐ[A] B) :=
by
refine ⟨⟨fun f g ↦ algEquiv_eq_of_apply_eq S A B fun n hn h1 ↦ ?_⟩⟩
obtain ⟨r, hr⟩ := ‹IsCyclotomicExtension S A B›.exists_isPrimitiveRoot hn h1
use r, hr
simp only [AlgEquiv.mul_apply]
have := NeZero.mk h1
obtain ⟨mf, -, hf⟩ := hr.eq_pow_of_pow_eq_one (show f r ^ n = 1 by rw [← map_pow, hr.1, map_one])
obtain ⟨mg, -, hg⟩ := hr.eq_pow_of_pow_eq_one (show g r ^ n = 1 by rw [← map_pow, hr.1, map_one])
simp [← hf, ← hg, ← pow_mul, mul_comm mf mg]
