map_dpow — Mathlib

English

If f is a DividedPowers morphism between hI and hJ, then f commutes with dpow on elements of I: f(hI.dpow n a) = hJ.dpow n (f(a)).

Русский

Если f — морфизм делённых степеней между hI и hJ, то он сохраняет делённые степени: f(dpow n a) = dpow n (f a) для a ∈ I.

LaTeX

$$$f(hI.dpow n a) = hJ.dpow n (f a)$$$

Lean4

theorem map_dpow {f : A →+* B} (hf : IsDPMorphism hI hJ f) {n : ℕ} {a : A} (ha : a ∈ I) :
    f (hI.dpow n a) = hJ.dpow n (f a) :=
  (hf.2 a ha).symm

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