exponent_def' — Mathlib

English

For any HasExponent K L and p with [ExpChar K p], and a ∈ L, a^{p^{exponent K L}} ∈ range(algebraMap K L).

Русский

Для HasExponent K L и p с [ExpChar K p], и a ∈ L, имеет место a^{p^{exponent K L}} ∈ диапазон algebraMap K L.

LaTeX

$$a^{p^{\text{exponent } K L}} ∈ \operatorname{range}(\operatorname{algebraMap} K L)$$

Lean4

/-- Version of `exponent_def` using `ExpChar`. -/
theorem exponent_def' [HasExponent K L] (p : ℕ) [ExpChar K p] (a : L) : a ^ p ^ exponent K L ∈ (algebraMap K L).range :=
  ringExpChar.eq K p ▸ exponent_def K a

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