English
An equivalence e transfers the MulZeroClass structure from β to α, i.e., α gains a MulZeroClass structure so that e preserves multiplication and zero.
Русский
Эквивеальность e переносит структуру MulZeroClass с β на α; т.е. α получает структуру MulZeroClass так, что e сохраняет умножение и нуль.
LaTeX
$$$\text{If } e:\alpha\simeq\beta\text{ and } [MulZeroClass\beta],\text{ then } [MulZeroClass\alpha]\text{ with } a\cdot_\alpha b := e^{-1}(e(a)\,e(b)),\ 0_\alpha := e^{-1}(0_β).$$$
Lean4
/-- Transfer `MulZeroClass` across an `Equiv` -/
protected abbrev mulZeroClass [MulZeroClass β] : MulZeroClass α :=
by
let zero := e.zero
let mul := e.mul
apply e.injective.mulZeroClass _ <;> intros <;> exact e.apply_symm_apply _
