abs_isAbsoluteValue

Mathlib.Algebra.Order.AbsoluteValue.Basic

URI: https://scilib.ai/kg/mathlib#IsAbsoluteValue.abs_isAbsoluteValue

English

The function abs on a ring is an absolute value, i.e., it satisfies the axioms of an absolute value.

Русский

Функция abs на кольце является абсолютной величиной, то есть удовлетворяет аксиомам абсолютной величины.

LaTeX

$$IsAbsoluteValue(abs : S → S)$$

Lean4

instance abs_isAbsoluteValue : IsAbsoluteValue (abs : S → S) :=
  AbsoluteValue.abs.isAbsoluteValue

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

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

Разделы

Аффилиация

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