isUnit_unop — Mathlib

English

Let M be a monoid. An element m of the opposite monoid M^op is a unit in M^op if and only if its unop lies as a unit in M.

Русский

Пусть M — моноид. Элемент m противоположного моноида M^op является единицей в M^op тогда и только тогда, когда его отображение в M под единицей является единицей.

LaTeX

$$$\forall m \in M^{\mathrm{op}}, \; \operatorname{IsUnit}(\operatorname{unop} m) \iff \operatorname{IsUnit}(m)$$$

Lean4

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

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