dpow_eq_of_mem — Mathlib

English

If a ∈ J, then (IsSubDPIdeal.dividedPowers hI hJ).dpow n a = hI.dpow n a for all n ∈ ℕ.

Русский

Если a ∈ J, то для всех n ∈ ℕ выполняется (IsSubDPIdeal.dividedPowers hI hJ).dpow n a = hI.dpow n a.

LaTeX

$$$(IsSubDPIdeal.dividedPowers hI hJ).dpow\, n\, a = hI.dpow n a \quad\text{при } a\in J$$$

Lean4

theorem dpow_eq_of_mem {n : ℕ} {a : A} (ha : a ∈ J) : (IsSubDPIdeal.dividedPowers hI hJ).dpow n a = hI.dpow n a := by
  rw [dpow_eq, if_pos ha]

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