elemExponent_le_exponent — Mathlib

English

For a ∈ L, if HasExponent K L holds, then elemExponent(K,a) ≤ exponent(K,L).

Русский

Для элементa a∈L при наличии HasExponent(K,L) выполняется elemExponent(K,a) ≤ exponent(K,L).

LaTeX

$$$ \operatorname{elemExponent}(K,a) \le \operatorname{exponent}(K,L) $$$

Lean4

/-- An exponent of an element is less or equal than exponent of the extension. -/
theorem elemExponent_le_exponent [HasExponent K L] (a : L) : elemExponent K a ≤ exponent K L :=
  elemExponent_le_of_pow_mem <| exponent_def K a

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