associated_one_of_mul_eq_one

Mathlib.Algebra.GroupWithZero.Associated

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

← MathLib Explorer

English

If a·b = 1 in a commutative monoid, then a is associated with 1.

Русский

Если a·b = 1 в коммутативном моноиде, то a связано с 1.

LaTeX

$$$ a b = 1 \\Rightarrow a ~ᵤ 1 $$$

Lean4

theorem associated_one_of_mul_eq_one [CommMonoid M] {a : M} (b : M) (hab : a * b = 1) : a ~ᵤ 1 :=
  show (Units.mkOfMulEqOne a b hab : M) ~ᵤ 1 from unit_associated_one

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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