nonUnitalNonAssocSemiring — Mathlib

English

Transfer a NonUnitalNonAssocSemiring structure across an Equiv: α inherits the structure from β via e.

Русский

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

LaTeX

$$$\text{protected abbrev nonUnitalNonAssocSemiring } [NonUnitalNonAssocSemiring\beta] : NonUnitalNonAssocSemiring\alpha$$$

Lean4

/-- Transfer `NonUnitalNonAssocSemiring` across an `Equiv` -/
protected abbrev nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring β] : NonUnitalNonAssocSemiring α :=
  by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalNonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

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