toMonoidWithZeroHom

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#AbsoluteValue.toMonoidWithZeroHom

English

There is a monoid-with-zero hom defined by AbsoluteValue from R to S: abv defines a MonoidWithZeroHom.

Русский

Существует гомоморфизм моноида с нулём, задаваемый AbsoluteValue: abv: R →*₀ S.

LaTeX

$$abv : AbsoluteValue R S → MonoidWithZeroHom R S$$

Lean4

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`. -/
def toMonoidWithZeroHom : R →*₀ S :=
  abv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru