iff_singleton — Mathlib

English

If IsCyclotomicExtension holds for a singleton {1}, then the image of A in B is the whole B (the subalgebra generated by A inside B is all of B).

Русский

Если IsCyclotomicExtension выполняется для единичного множества {1}, то образ A в B равен всем B.

LaTeX

$$IsCyclotomicExtension \\{1\\} A B \\implies (A \\to B) is surjective$$

Lean4

/-- A reformulation of `IsCyclotomicExtension` in the case `S` is a singleton. -/
theorem iff_singleton :
    IsCyclotomicExtension { n } A B ↔ (∃ r : B, IsPrimitiveRoot r n) ∧ ∀ x, x ∈ adjoin A {b : B | b ^ n = 1} := by
  simp [isCyclotomicExtension_iff, NeZero.ne]

Похожие утверждения