exponent_eq_one_iff — Mathlib

English

This restates that exponent θ equals 1 iff the subring generated by θ over ℤ equals the whole ring of integers 𝓞K.

Русский

Это переформулировка: exponent θ = 1 тогда и только тогда, если подсистема, порождаемая θ над ℤ, равна всему 𝓞K.

LaTeX

$$$\\text{exponent}(θ) = 1 \\iff \\langle \\mathbb{Z}, θ \\rangle = \\mathcal{O}_K$$$

Lean4

theorem exponent_eq_one_iff : exponent θ = 1 ↔ Algebra.adjoin ℤ { θ } = ⊤ := by
  rw [exponent, absNorm_eq_one_iff, comap_eq_top_iff, conductor_eq_top_iff_adjoin_eq_top]

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