nonAssocSemiring — Mathlib

English

Transfer NonAssocSemiring across an Equiv: α inherits NonAssocSemiring structure from β via e.

Русский

Переносим NonAssocSemiring через эквивалентность: α наследует NonAssocSemiring от β через e.

LaTeX

$$$\text{protected abbrev nonAssocSemiring } [NonAssocSemiring \beta] : NonAssocSemiring \alpha$$$

Lean4

/-- Transfer `NonAssocSemiring` across an `Equiv` -/
protected abbrev nonAssocSemiring [NonAssocSemiring β] : NonAssocSemiring α :=
  by
  let mul := e.mul
  let add_monoid_with_one := e.addMonoidWithOne
  apply e.injective.nonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

Похожие утверждения