mapDomainRingHom_comp — Mathlib

English

A further compatibility: the composition of mapRangeRingHom with mapDomainRingHom equals the swapped composition, i.e., (mapRangeRingHom N f) ∘ (mapDomainRingHom R g) = (mapDomainRingHom S g) ∘ (mapRangeRingHom M f).

Русский

Дополнительная совместимость: компоновка mapRangeRingHom с mapDomainRingHom равна переставленной компоновке, т.е. (mapRangeRingHom N f) ∘ (mapDomainRingHom R g) = (mapDomainRingHom S g) ∘ (mapRangeRingHom M f).

LaTeX

$$$ (mapRangeRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRangeRingHom M f) $$$

Lean4

@[to_additive (dont_translate := R) (attr := simp)]
theorem mapDomainRingHom_comp (f : N →* O) (g : M →* N) :
    mapDomainRingHom R (f.comp g) = (mapDomainRingHom R f).comp (mapDomainRingHom R g) := by ext <;> simp

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