English
There is an equivalence between MulEquiv α β and MulEquiv α^op β^op given by the opposite operation; this respects the multiplicative structure.
Русский
Существует эквиваленция между MulEquiv α β и MulEquiv α^op β^op, задаваемая операцией противоположности; она сохраняет умножение.
LaTeX
$$$\\mathrm{MulEquiv}(α,β) \\simeq \\mathrm{MulEquiv}(α^{op}, β^{op})$$$
Lean4
/-- An iso `α ≃* β` can equivalently be viewed as an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. -/
@[to_additive (attr := simps) /-- An iso `α ≃+ β` can equivalently be viewed as an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`. -/
]
def op {α β} [Mul α] [Mul β] : α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)
where
toFun
f :=
{ toFun := MulOpposite.op ∘ f ∘ unop, invFun := MulOpposite.op ∘ f.symm ∘ unop,
left_inv x := unop_injective (f.symm_apply_apply x.unop),
right_inv x := unop_injective (f.apply_symm_apply x.unop),
map_mul' x y := unop_injective (map_mul f y.unop x.unop) }
invFun
f :=
{ toFun := unop ∘ f ∘ MulOpposite.op, invFun := unop ∘ f.symm ∘ MulOpposite.op, left_inv x := by simp,
right_inv x := by simp, map_mul' x y := congr_arg unop (map_mul f (MulOpposite.op y) (MulOpposite.op x)) }
