map_one_of_isLeftRegular

Mathlib.Algebra.Order.AbsoluteValue.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem map_one_of_isLeftRegular (h : IsLeftRegular (abv 1)) : abv 1 = 1 :=
  h <| by simp [← abv.map_mul]

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

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

Разделы

Аффилиация

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