mkRingHom — Mathlib

English

There is a natural ring hom from R to SeparationQuotient(R) sending r to mk(r); it preserves addition and multiplication and sends 0 to 0 and 1 to 1 when available.

Русский

Существует естественный кольцевой гомоморфизм из R в SeparationQuotient(R), отображающий r в mk(r) и сохраняющий сложение и умножение (а также 0 и 1 при наличии единицы).

LaTeX

$$$\mk : R \to+* \mathrm{SeparationQuotient}(R)$$$

Lean4

/-- `SeparationQuotient.mk` as a `RingHom`. -/
@[simps]
def mkRingHom [NonAssocSemiring R] [IsTopologicalSemiring R] : R →+* SeparationQuotient R
    where
  toFun := mk
  map_one' := mk_one; map_zero' := mk_zero; map_add' := mk_add; map_mul' := mk_mul

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