English
The absolute value on ℝ, viewed as a map to ℝ≥0, is a monoid hom from (ℝ, ×) to (ℝ≥0, ×).
Русский
Абсолютное значение на ℝ, рассматриваемое как отображение в ℝ≥0, является гомоморфизмом умножения от (ℝ, ×) к (ℝ≥0, ×).
LaTeX
$$$ \mathrm{nnabs}: \mathbb{R} \to \mathbb{R}_{\ge 0} \text{ is a monoid with zero hom}, \\ \mathrm{nnabs}(xy) = \mathrm{nnabs}(x) \mathrm{nnabs}(y), \ \mathrm{nnabs}(0) = 0, \ \mathrm{nnabs}(1) = 1. $$$
Lean4
/-- The absolute value on `ℝ` as a map to `ℝ≥0`. -/
@[pp_nodot]
def nnabs : ℝ →*₀ ℝ≥0 where
toFun x := ⟨|x|, abs_nonneg x⟩
map_zero' := by ext; simp
map_one' := by ext; simp
map_mul' x y := by ext; simp [abs_mul]
