exists_eq_pow_p_mul' — Mathlib

English

For a Witt vector a ≠ 0 in 𝕎 k and a perfect ring of characteristic p, there exist m and a unit b such that a = (p)^m · b.

Русский

Для не нуля вектора Витта a в 𝕎 k и совершенного кольца с характеристикой p существуют m и единица b such that a = p^m · b.

LaTeX

$$$\exists m\, \exists b\, a = (p : 𝕎 k)^m \cdot b$$$

Lean4

theorem exists_eq_pow_p_mul' (a : 𝕎 k) (ha : a ≠ 0) : ∃ (m : ℕ) (b : Units (𝕎 k)), a = (p : 𝕎 k) ^ m * b :=
  by
  obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha
  let b₀ := Units.mk0 (b.coeff 0) h₁
  have hb₀ : b.coeff 0 = b₀ := rfl
  exact ⟨m, mkUnit hb₀, h₂⟩

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