map_one

Mathlib.Algebra.Order.AbsoluteValue.Basic

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

English

If abv(1) is left-regular, then abv(1) = 1. (repeat)

Русский

Если abv(1) левая регулярность, то abv(1)=1. (повтор)

LaTeX

$$$\text{IsLeftRegular}(abv(1))\Rightarrow abv(1)=1$$$

Lean4

@[simp]
protected theorem map_one : abv 1 = 1 :=
  abv.map_one_of_isLeftRegular (isRegular_of_ne_zero <| abv.ne_zero one_ne_zero).left

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

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

Разделы

Аффилиация

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