divisionCommMonoid — Mathlib

English

The Interval α has a DivisionCommMonoid structure extending the commutative monoid, with the division operation defined by x / y and the corresponding identities held.

Русский

Interval α имеет структуру DivisionCommMonoid, расширяющую коммутативный моноид; операция деления определена как x / y и выполняются соответствующие тождественные свойства.

LaTeX

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

Lean4

@[to_additive existing Interval.subtractionCommMonoid]
instance divisionCommMonoid : DivisionCommMonoid (Interval α) :=
  { Interval.commMonoid with
    inv := Inv.inv
    div := (· / ·)
    div_eq_mul_inv := by
      rintro (_ | s) (_ | t) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (div_eq_mul_inv _ _)
    inv_inv := by
      rintro (_ | s) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (inv_inv _)
    mul_inv_rev := by
      rintro (_ | s) (_ | t) <;>
        first
        | rfl
        | exact congr_arg WithBot.some (mul_inv_rev _ _)
    inv_eq_of_mul := by
      rintro (_ | s) (_ | t) h <;>
        first
        | cases h
        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h) }

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