English
Two elements of the Galois group p.Gal are equal if and only if they agree on all roots of p in the splitting field.
Русский
Две фермы p.Gal равны тогда и только тогда, когда они совпадают на всех корнях p в поле разложения.
LaTeX
$$$\text{theorem }\mathrm{ext}:\; \forall \sigma,\tau\in p.Gal,\; (\forall x\in p.rootSet p.SplittingField, \sigma x=\tau x)\Rightarrow \sigma=\tau.$$$
Lean4
@[ext]
theorem ext {σ τ : p.Gal} (h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x) : σ = τ :=
by
refine
AlgEquiv.ext fun x =>
(AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp ((SetLike.ext_iff.mp ?_ x).mpr Algebra.mem_top)
rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]
