monoidWithZeroHomClass — Mathlib

English

The family of AbsoluteValue maps forms a MonoidWithZeroHomClass from R to S; in particular, they preserve multiplication, zero, and one.

Русский

Множество отображений AbsoluteValue образует MonoidWithZeroHomClass от R к S; в частности, сохраняются умножение, ноль и единица.

LaTeX

$$MonoidWithZeroHomClass(AbsoluteValue R S) R S$$

Lean4

instance monoidWithZeroHomClass : MonoidWithZeroHomClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.mulHomClass with
    map_zero := fun f => f.map_zero
    map_one := fun f => f.map_one }

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