English
Let e: α ≃ β be a type equivalence. If β is a Semiring, then α can be given a Semiring structure by transporting all ring operations along e; in particular, the addition, multiplication, zero and one on α are defined so that e becomes a Semiring isomorphism α ≃ β.
Русский
Пусть e: α ≃ β — эквивалентность множеств. Если β имеет структуру полугольника, то α наделяется структурой полугольника, полученной переносом операций вдоль e; в частности, операции сложения и умножения, ноль и единица на α задаются так, чтобы e была полугольным изоморфизмом α ≃ β.
LaTeX
$$$(\alpha, +_\alpha, \cdot_\alpha, 0_\alpha, 1_\alpha)$ содержит определения $x +_\alpha y := e^{-1}(e x + e y)$, $x \cdot_\alpha y := e^{-1}(e x \cdot e y)$, $0_\alpha := e^{-1}(0)$, $1_\alpha := e^{-1}(1)$; hence $(\alpha, +_\alpha, \cdot_\alpha, 0_\alpha, 1_\alpha)$ is a Semiring and $e: \alpha \to \beta$ is a Semiring isomorphism.$$
Lean4
/-- Transfer `Semiring` across an `Equiv` -/
protected abbrev semiring [Semiring β] : Semiring α :=
by
let mul := e.mul
let add_monoid_with_one := e.addMonoidWithOne
let npow := e.pow ℕ
apply e.injective.semiring _ <;> intros <;> exact e.apply_symm_apply _
