coe_opEquiv_symm — Mathlib

English

The symm of opEquiv maps a unit in the opposite to the corresponding op of its unop.

Русский

Обратное к opEquiv переводит единицу в противоположность к соответствующему op её развёрнутому значению.

LaTeX

$$$\\text{Units}.coe\_opEquiv\\_symm(u) : M^{\\mathrm{op}} \\to M$ satisfies the expected equality.$$

Lean4

@[to_additive (attr := simp)]
theorem coe_opEquiv_symm {M} [Monoid M] (u : Mˣᵐᵒᵖ) : (Units.opEquiv.symm u : Mᵐᵒᵖ) = op (u.unop : M) :=
  rfl

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