English
An equivalence e: α ≃ β transfers a SemigroupWithZero structure from β to α via x · y = e⁻¹(e x · e y) and 0α = e⁻¹(0β), making e an isomorphism of semigroups with zero.
Русский
Эквивелентность e: α ≃ β переносит структуру SemigroupWithZero с β на α через x · y = e⁻¹(e x · e y) и 0α = e⁻¹(0β), так что e становится изоморфизмом полугрупп с нулём.
LaTeX
$$$\text{If } e:\alpha\simeq\beta,\ [\text{SemigroupWithZero }\beta],\text{ then } \text{SemigroupWithZero }\alpha \text{ with } x\cdot_\alpha y := e^{-1}(e(x)\cdot e(y)),\ 0_\alpha := e^{-1}(0_β).$$$
Lean4
/-- Transfer `SemigroupWithZero` across an `Equiv` -/
protected abbrev semigroupWithZero [SemigroupWithZero β] : SemigroupWithZero α :=
by
let mul := e.mul
let zero := e.zero
apply e.injective.semigroupWithZero _ <;> intros <;> exact e.apply_symm_apply _
