isUnit_mul_self_iff

Mathlib.Algebra.Group.Commute.Units

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

English

For any a in a monoid, IsUnit (a a) iff IsUnit a.

Русский

Для любого a в моноиде, IsUnit (a a) эквивалентно IsUnit a.

LaTeX

$$IsUnit (a \cdot a) \Leftrightarrow IsUnit a$$

Lean4

@[to_additive (attr := simp)]
theorem isUnit_mul_self_iff : IsUnit (a * a) ↔ IsUnit a :=
  (Commute.refl a).isUnit_mul_iff.trans and_self_iff

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

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

Разделы

Аффилиация

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