exponent — Mathlib

English

The exponent of a purely inseparable extension is the least e ∈ ℕ such that a^{p^e} ∈ K for all a ∈ L.

Русский

Показатель разложения — минимальное e ∈ ℕ такое, что для всех a ∈ L выполняется a^{p^e} ∈ K.

LaTeX

$$exponent K L = min\{ e ∈ ℕ : ∀ a ∈ L, a^{p^e} ∈ K \}$$

Lean4

/-- The *exponent* of a purely inseparable extension is the smallest
natural number `e` such that `a ^ ringExpChar K ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [HasExponent K L] : ℕ :=
  Nat.find ‹HasExponent K L›.has_exponent

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