instNonUnitalNonAssocSemiring — Mathlib

English

If α is a NonUnitalNonAssocSemiring with compatible order and CanonicallyOrderedAdd, then WithTop α carries a corresponding NonUnitalNonAssocSemiring structure extending that of α.

Русский

Если α — полуп ring без единицы без ассоциативности с совместимым порядком и канонически упорядоченным сложением, то WithTop α получает соответствующую структуру NonUnitalNonAssocSemiring, расширяющую α.

LaTeX

$$$\\text{WithTop }\\alpha \\\\text{ is a NonUnitalNonAssocSemiring given } \\alpha \\\\text{ is}$$$

Lean4

instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] :
    NonUnitalNonAssocSemiring (WithTop α)
    where
  toAddCommMonoid := WithTop.addCommMonoid
  __ := WithTop.instMulZeroClass
  right_distrib a b
    c := by
    cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)
  left_distrib c a
    b := by
    cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [coe_mul_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (mul_add _ _ _)

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