instNonAssocSemiring — Mathlib

English

Under similar hypotheses, SkewMonoidAlgebra k G inherits a NonAssocSemiring structure, i.e., a semiring without the associativity constraint required globally, due to the skew/noncommutative action.

Русский

При аналогичных предположениях SkewMonoidAlgebra k G наследует структуру NonAssocSemiring (полугруппа без требуемой ассоциативности).

LaTeX

$$$\ SkewMonoidAlgebra k G \text{ is a NonAssocSemiring}. $$$

Lean4

instance : NonAssocSemiring (SkewMonoidAlgebra k G)
    where
  one_mul
    f := by
    induction f with
    | single g a => rw [one_def, mul_def, sum_single_index] <;> simp
    | add f g _ _ => simp_all [mul_add]
  mul_one
    f := by
    induction f with
    | single g a => rw [one_def, mul_def, sum_single_index, sum_single_index] <;> simp
    | add f g _ _ => simp_all [add_mul]

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