associated_one_of_associated_mul_one

Mathlib.Algebra.GroupWithZero.Associated

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

← MathLib Explorer

English

If a.b ~ᵤ 1 in a commutative monoid, then a ~ᵤ 1.

Русский

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

LaTeX

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

Lean4

theorem associated_one_of_associated_mul_one [CommMonoid M] {a b : M} : a * b ~ᵤ 1 → a ~ᵤ 1
  | ⟨u, h⟩ => associated_one_of_mul_eq_one (b * u) <| by simpa [mul_assoc] using h

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

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

Разделы

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

Аффилиация

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