isUnit_op

Mathlib.Algebra.Group.Units.Opposite

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

English

For any monoid M, IsUnit (op m) holds iff IsUnit m.

Русский

Для любого моноида M: IsUnit (оп m) равно IsUnit m.

LaTeX

$$$\\text{IsUnit}(\\mathrm{op}\\, m) \\iff \\text{IsUnit}(m)$$$

Lean4

@[to_additive (attr := simp)]
theorem isUnit_op {M} [Monoid M] {m : M} : IsUnit (op m) ↔ IsUnit m :=
  ⟨IsUnit.unop, IsUnit.op⟩

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

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

Разделы

Аффилиация

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