English
An equivalence transfers CommMonoidWithZero structure from β to α, i.e., α becomes a commutative monoid with zero under the transported operations, with e a isomorphism.
Русский
Эквивиальность переносит CommMonoidWithZero структуру с β на α; α становится коммутативным моноидом с нулём под переносимыми операциями, и e образует изоморфизм.
LaTeX
$$$\forall e:\alpha\simeq\beta,\ [CommMonoidWithZero\beta]\Rightarrow [CommMonoidWithZero\alpha],\text{ с } a\cdot_\alpha b := e^{-1}(e(a)\,e(b)),\ 0_\alpha := e^{-1}(0_β),\ 1_\alpha := e^{-1}(1_β).$$$
Lean4
/-- Transfer `CommMonoidWithZero` across an `Equiv` -/
protected abbrev commMonoidWithZero [CommMonoidWithZero β] : CommMonoidWithZero α :=
by
let _ := e.monoidWithZero
apply e.injective.commMonoidWithZero _ <;> intros <;> exact e.apply_symm_apply _
