isUnit_iff_eq_bot

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.isUnit_iff_eq_bot

English

IsUnit(a) iff a equals the bottom element ⊥ in Associates M.

Русский

IsUnit(a) ⇔ a = ⊥ в Associates(M).

LaTeX

$$$ \operatorname{IsUnit}(a) \iff a = \bot $$$

Lean4

theorem isUnit_iff_eq_bot {a : Associates M} : IsUnit a ↔ a = ⊥ := by rw [Associates.isUnit_iff_eq_one, bot_eq_one]

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

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

Разделы

Аффилиация

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