dpow_comp_from_gens — Mathlib

English

Suppose I = span S and f maps S into J and preserves dpow on S. Then for every n and a ∈ I, hJ.dpow n (f a) = f(hI.dpow n a).

Русский

Пусть I = span S и f отображает S в J и сохраняет dpow на S. Тогда для любого n и a ∈ I выполняется hJ.dpow n (f a) = f(hI.dpow n a).

LaTeX

$$$\\forall {n}, \\forall a \\in I, hJ.dpow n (f a) = f (hI.dpow n a)$$$

Lean4

theorem dpow_comp_from_gens {S : Set A} (hS : I = span S) (hS' : ∀ s ∈ S, f s ∈ J)
    (hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) : ∀ {n}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a) :=
  (IsDPMorphism.on_span hI hJ hS hS' hdp).2

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