dpow_of_two_le — Mathlib

English

If I^2 = 0 and 2 ≤ n, then for all a ∈ A, the n-th divided power of a equals 0.

Русский

Если I^2 = 0 и 2 ≤ n, то для любого a ∈ A n-я разделённая степень равна 0.

LaTeX

$$$I^2 = 0 \Rightarrow 2 \le n \Rightarrow (dividedPowers I).dpow n a = 0$$$

Lean4

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

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