English
For domain B, given primitive root ζ of order n, the adjunction of all roots of cyclotomic n in B equals adjunction of all elements b with ∃ a = n, a ≠ 0, b^a = 1.
Русский
Для области B и примитивного корня ζ порядка n равняется адъюнкция всех корней циклотомического многочлена Φ_n равной адъюнкции всех элементов b с ∃ a = n, a ≠ 0, b^a = 1.
LaTeX
$$$IsDomain(B) \\Rightarrow (ζ \\text{ примитивный корень } n) \\Rightarrow \\\\ Algebra.adjoin\\ A ((Φ_n(A)).rootSet B) = Algebra.adjoin\\ A\\{ b \\in B \\mid \\exists a\\ (a=n) \\land a \\neq 0 \\land b^a=1\\}$$$
Lean4
/-- Two elements in the Galois group of a cyclotomic extension are equal if
their actions on primitive roots are equal. -/
theorem algEquiv_eq_of_apply_eq [IsCyclotomicExtension S A B] [IsDomain B] {f g : B ≃ₐ[A] B}
(H : ∀ n ∈ S, n ≠ 0 → ∃ r : B, IsPrimitiveRoot r n ∧ f r = g r) : f = g :=
by
ext x
have hx := ‹IsCyclotomicExtension S A B›.adjoin_roots x
induction hx using Algebra.adjoin_induction with
| mem y hy =>
obtain ⟨n, hn, h1, h2⟩ := hy
obtain ⟨r, hr1, hr2⟩ := H n hn h1
have := NeZero.mk h1
obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
simp [hr2]
| algebraMap y => simp
| add x y hx hy ihx ihy => simp [ihx, ihy]
| mul x y hx hy ihx ihy => simp [ihx, ihy]
