English
The noncomputable liftRight construction provides a map M →* Nˣ whenever every f x is a unit, extending f to the units of N.
Русский
Конструкция liftRight (невычислимая) задаёт отображение M →* Nˣ, если для всех x произведение f(x) — единица, и она расширяет f до единиц N.
LaTeX
$$$\\text{IsUnit.liftRight}(f,hf) : M \\to^* N^{\\times}$$$
Lean4
/-- The units of the opposites are equivalent to the opposites of the units. -/
@[to_additive /-- The additive units of the additive opposites are equivalent to the additive opposites
of the additive units. -/
]
def opEquiv {M} [Monoid M] : Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ
where
toFun u := op ⟨unop u, unop ↑u⁻¹, op_injective u.4, op_injective u.3⟩
invFun := MulOpposite.rec' fun u => ⟨op ↑u, op ↑u⁻¹, unop_injective <| u.4, unop_injective u.3⟩
map_mul' _ _ := unop_injective <| Units.ext <| rfl
