unop

Mathlib.Algebra.Group.Units.Opposite

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\\text{IsUnit}(\\mathrm{unop} \\, m) \\Rightarrow \\text{IsUnit}(m)$ for m ∈ Mᵐᵒᵖ.$$

Lean4

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

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

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

Разделы

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

Аффилиация

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