map_range — Mathlib

English

Mapping the range along another ring homomorphism g: S →+* T yields the range of the composed map g ∘ f.

Русский

Преобразование образа через гомоморфизм g: S →+* T даёт образ композиции g ∘ f.

LaTeX

$$$\\mathrm{range}(g \\circ f) = \\mathrm{Subring.map}(g)(\\mathrm{range}(f))$$$

Lean4

theorem map_range : f.range.map g = (g.comp f).range := by simpa only [range_eq_map] using (⊤ : Subring R).map_map g f

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