nonUnitalNonAssocSemiring — Mathlib

English

The structure MonoidAlgebra R M carries the structure of a NonUnitalNonAssocSemiring: it has a bilinear multiplication with distributivity and a zero, but no requirement of a multiplicative identity.

Русский

У структуры MonoidAlgebra R M есть структура NonUnitalNonAssocSemiring: есть умножение, распределённость и ноль, но единицы умножения нет.

LaTeX

$$$\operatorname{NonUnitalNonAssocSemiring}(\operatorname{MonoidAlgebra} \; R \; M)$$$

Lean4

@[to_additive (dont_translate := R)]
instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (MonoidAlgebra R M)
    where
  zero_mul := by simp [mul_def]
  mul_zero := by
    simp [mul_def]
      -- Porting note: `refine` & `exact` are required because `simp` behaves differently.

  left_distrib f g
    h := by
    classical
    simp only [mul_def]
    refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
      simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
  right_distrib f g
    h := by
    classical
    simp only [mul_def]
    refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
      simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

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