dpow_eq — Mathlib

English

Let I be a divisor-power structure on A and J a sub-dp-ideal determined by hI and hJ. Then for every n ∈ ℕ and a ∈ A, the dpow of the constructed object equals hI.dpow n a if a ∈ J, and equals 0 otherwise.

Русский

Пусть I задаёт структуру делённых степеней на A и J является под dp-идеалом, определённым через hI и hJ. Тогда для каждого n ∈ ℕ и каждого a ∈ Adpow-операция даёт значения: равно hI.dpow n a при a ∈ J и нулю при a ∉ J.

LaTeX

$$$(\text{DividedPowers.IsSubDPIdeal.dividedPowers } hI hJ).dpow\, n\, a = \begin{cases} hI.dpow\, n\, a, & a \in J \\ 0, & a \notin J \end{cases}$$$

Lean4

theorem dpow_eq (n : ℕ) (a : A) : (IsSubDPIdeal.dividedPowers hI hJ).dpow n a = if a ∈ J then hI.dpow n a else 0 :=
  rfl

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