map_mrange — Mathlib

English

For g : N →* P and f : M →* N, we have (mrange f).map g = mrange (g.comp f).

Русский

Для гомоморфизмов g : N →* P и f : M →* N имеем (mrange f).map g = mrange (g.comp f).

LaTeX

$$$$ (\\mathrm{mrange}\;f).\\mathrm{map}\;g = \\mathrm{mrange}(g \\circ f) $$$$

Lean4

@[to_additive]
theorem map_mrange (g : N →* P) (f : M →* N) : (mrange f).map g = mrange (comp g f) := by
  simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

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