exponent — Mathlib

English

For θ in the ring of integers, the exponent θ equals 1 if and only if the ℤ-algebra generated by θ is the whole ring of integers; equivalently, the smallest subalgebra of 𝓞K containing θ is the entire ring.

Русский

Для θ в 𝓞K показатель exponent θ равен 1 тогда и только тогда, когда ℤ[θ] порождает всю 𝓞K.

LaTeX

$$$\\text{exponent}(θ) = 1 \\;\\Longleftrightarrow\\; \\mathbb{Z}[\\,θ\\] = \\mathcal{O}_K.$$$

Lean4

/-- The smallest positive integer `d` contained in the conductor of `θ`. It is the smallest integer
such that `d • 𝓞 K ⊆ ℤ[θ]`, see `exponent_eq_sInf`. It is set to `0` if `d` does not exists.
-/
def exponent (θ : 𝓞 K) : ℕ :=
  absNorm (under ℤ (conductor ℤ θ))

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