English
If A is a commutative semiring-like algebra over R, then Aᵐᵒᵖ carries a canonical R-algebra structure, reversing multiplication inside A.
Русский
У Aᵐᵒᵖ над R имеется естественная структура R-алгебры, полученная за счёт обращения умножения.
LaTeX
$$Aᵐᵒᵖ is an Algebra R over A with reversed multiplication$$
Lean4
instance instAlgebra : Algebra R Aᵐᵒᵖ
where
algebraMap := (algebraMap R A).toOpposite fun _ _ => Algebra.commutes _ _
smul_def' c
x :=
unop_injective <| by
simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, Algebra.smul_def, Algebra.commutes,
unop_op]
commutes'
r :=
MulOpposite.rec' fun x => by simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]
