English
Let e: α ≃ β be an equivalence and assume β is a NonUnitalCommutative Semiring. Then α inherits a NonUnitalCommSemiring structure transported along e, with e as a homomorphism of the transported structure.
Русский
Пусть e: α ≃ β — эквивалентность и β обладает структурой NonUnitalCommSemiring. Тогда α получает структуру NonUnitalCommSemiring, полученную переносом через e, причём e сохраняет перенесённую структуру.
LaTeX
$$$(\alpha, +_\alpha, \cdot_\alpha) \\text{ with } x +_\alpha y := e^{-1}(e x + e y), \; x \cdot_\alpha y := e^{-1}(e x \cdot e y)$, и $(\alpha, +_\alpha, \cdot_\alpha)$ образует NonUnitalCommSemiring с изоморфизмом $e$ на β.$$
Lean4
/-- Transfer `NonUnitalCommSemiring` across an `Equiv` -/
protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring β] : NonUnitalCommSemiring α :=
by
let zero := e.zero
let add := e.add
let mul := e.mul
let nsmul := e.smul ℕ
apply e.injective.nonUnitalCommSemiring _ <;> intros <;> exact e.apply_symm_apply _
