English
If two subalgebras C1 and C2 both form IsCyclotomicExtension S A C1 and S A C2, then C1 = C2.
Русский
Если два подполья C1 и C2 образуют IsCyclotomicExtension S A C1 и S A C2, то C1 = C2.
LaTeX
$$$\\text{If } C_1,C_2:\\; \\text{IsCyclotomicExtension}(S,A,C_1) \\text{ and } \\text{IsCyclotomicExtension}(S,A,C_2),\\; \\; C_1=C_2$$$
Lean4
theorem eq (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension S A C₁] [h₂ : IsCyclotomicExtension S A C₂] : C₁ = C₂ :=
by
have hC (n) (hn₁ : n ∈ S) (hn₂ : n ≠ 0) : ∃ x : B, IsPrimitiveRoot x n :=
by
obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩
rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁, (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂]
