subtractionCommMonoid — Mathlib

English

The Interval α carries a subtraction commutative monoid structure, with neg and sub defined pointwise from α, and the usual subtraction laws hold.

Русский

Interval α несет структуру вычитательного коммутативного моноида, где отрицание и вычитание определяются покомпонентно из α и выполняются законы вычитания.

LaTeX

$$$ \text{SubtractionCommMonoid}(\text{Interval}(\alpha)) $$$

Lean4

instance subtractionCommMonoid {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :
    SubtractionCommMonoid (Interval α) :=
  { Interval.addCommMonoid with
    neg := Neg.neg
    sub := Sub.sub
    sub_eq_add_neg := by
      rintro (_ | s) (_ | t) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (sub_eq_add_neg _ _)
    neg_neg := by
      rintro (_ | s) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (neg_neg _)
    neg_add_rev := by
      rintro (_ | s) (_ | t) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (neg_add_rev _ _)
    neg_eq_of_add := by
      rintro (_ | s) (_ | t) h <;>
        first
        | cases h
        |
          exact
            congr_arg WithBot.some
              (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
                -- TODO: use a better defeq

    zsmul := zsmulRec }

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