nonUnitalSemiring — Mathlib

English

Transfer NonUnitalSemiring across an Equiv: α inherits the NonUnitalSemiring structure from β along e.

Русский

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

LaTeX

$$$\text{protected abbrev nonUnitalSemiring } [NonUnitalSemiring \beta] : NonUnitalSemiring \alpha$$$

Lean4

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

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