quotientKerEquivRange — Mathlib

English

Reaffirmation: the map homomorphism preserves multiplication: (x*y).map f = (x.map f) * (y.map f).

Русский

Поддерживается сохранение умножения при отображении: (x*y).map f = (x.map f) * (y.map f).

LaTeX

$$$ (x*y).map f = (x.map f) * (y.map f) $$$

Lean4

/-- The **first isomorphism theorem** for commutative rings (`RingHom.range` version). -/
noncomputable def quotientKerEquivRange (f : R →+* S) : R ⧸ ker f ≃+* f.range :=
  (Ideal.quotEquivOfEq f.ker_rangeRestrict.symm).trans <| quotientKerEquivOfSurjective f.rangeRestrict_surjective

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