English
Let e: α ≃ β be an equivalence and β a CommSemiring. Then α inherits a CommSemiring structure transported along e, with e as a Semiring isomorphism.
Русский
Пусть e: α ≃ β — эквивалентность и β — коммутативное полугольное кольцо. Тогда α наделяется переносной через e структурой CommSemiring, и 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)$; структуру на \alpha образует CommSemiring, и $e: \alpha \to \beta$ является его коммутативным полугруппным гомоморфизм.$$
Lean4
/-- Transfer `CommSemiring` across an `Equiv` -/
protected abbrev commSemiring [CommSemiring β] : CommSemiring α :=
by
let mul := e.mul
let add_monoid_with_one := e.addMonoidWithOne
let npow := e.pow ℕ
apply e.injective.commSemiring _ <;> intros <;> exact e.apply_symm_apply _
