divp_eq_one_iff_eq

Mathlib.Algebra.Group.Units.Basic

URI: https://scilib.ai/kg/mathlib#divp_eq_one_iff_eq

English

Let α be a monoid and u a unit in α. Then a /ₚ u = 1 if and only if a = u.

Русский

Пусть α — моноид и u — единица в α. Тогда a /ₚ u = 1 тогда и только тогда, когда a = u.

LaTeX

$$$ a \cdot u^{-1} = 1 \Leftrightarrow a = u $$$

Lean4

theorem divp_eq_one_iff_eq {a : α} {u : αˣ} : a /ₚ u = 1 ↔ a = u :=
  (Units.mul_left_inj u).symm.trans <| by rw [divp_mul_cancel, one_mul]

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

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

Разделы

Аффилиация

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