mem_span_pow_iff_le_valuation — Mathlib

English

For nonzero x in Z_p and n ∈ N, x lies in the ideal generated by p^n if and only if n ≤ v_p(x).

Русский

Для ненулевого x в Z_p и n ∈ N принадлежит ли x к идеалу, порождаемому p^n, эквивалентно тому, что n ≤ v_p(x).

LaTeX

$$$\forall x \in \mathbb{Z}_p,\ x \neq 0,\ \forall n \in \mathbb{N},\ x \in \operatorname{span}\{p^n\} \iff n \le v_p(x).$$$

Lean4

theorem mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
    x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) ↔ n ≤ x.valuation :=
  by
  rw [Ideal.mem_span_singleton]
  constructor
  · rintro ⟨c, rfl⟩
    suffices c ≠ 0 by
      rw [valuation_p_pow_mul _ _ this]
      exact le_self_add
    contrapose! hx
    rw [hx, mul_zero]
  · nth_rewrite 2 [unitCoeff_spec hx]
    simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _

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