isUnit_mk

Mathlib.Algebra.GroupWithZero.Associated

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

← MathLib Explorer

English

IsUnit(mk(a)) iff IsUnit(a).

Русский

IsUnit(Associates.mk(a)) ⇔ IsUnit(a).

LaTeX

$$$ \operatorname{IsUnit}( \operatorname{Associates.mk}(a) ) \iff \operatorname{IsUnit}(a) $$$

Lean4

theorem isUnit_mk {a : M} : IsUnit (Associates.mk a) ↔ IsUnit a :=
  calc
    IsUnit (Associates.mk a) ↔ a ~ᵤ 1 := by rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
    _ ↔ IsUnit a := associated_one_iff_isUnit

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

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

Разделы

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

Аффилиация

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