op

Mathlib.Algebra.Group.Units.Opposite

URI: https://scilib.ai/kg/mathlib#IsUnit.op

English

If m is a unit in M, then op m is a unit in Mᵐᵒᵖ.

Русский

Если m — единица в M, то op m — единица в Mᵐᵒᵖ.

LaTeX

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

Lean4

@[to_additive]
nonrec theorem op {M} [Monoid M] {m : M} (h : IsUnit m) : IsUnit (op m) :=
  let ⟨u, hu⟩ := h
  hu ▸ ⟨Units.opEquiv.symm (op u), rfl⟩

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

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

Разделы

Аффилиация

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