dpow_of_prime_le — Mathlib

English

In the CharP setting with p prime, and hIp: I^p = 0, the p-divided powers vanish beyond p.

Русский

В условии CharP с простым p и hIp: I^p = 0, разделённые степени по p исчезают за пределами p.

LaTeX

$$$p \text{ prime} \land hIp : I^p = 0 \Rightarrow (dividedPowers I).dpow n a = 0 \text{ for } p \le n$$$

Lean4

theorem dpow_of_prime_le {n : ℕ} (hn : p ≤ n) (a : A) : (dividedPowers A p hIp) n a = 0 :=
  by
  simp only [dividedPowers, IsNilpotent.dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]
  intro ha
  rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]

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