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