mapRangeRingHom_comp_mapDomainRingHom

English

A symmetry of maps: (mapRangeRingHom N f) ∘ (mapDomainRingHom R g) equals (mapDomainRingHom S g) ∘ (mapRangeRingHom M f).

Русский

Симметрия отображений: (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 S)]
theorem mapRangeRingHom_comp_mapDomainRingHom (f : R →+* S) (g : M →* N) :
    (mapRangeRingHom N f).comp (mapDomainRingHom R g) = (mapDomainRingHom S g).comp (mapRangeRingHom M f) := by aesop

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