English
The collection of intervals on α possesses a DivisionCommMonoid structure extending the additive structure, with division defined as x / y and inverse as x^{-1}.
Русский
Множество интервалов над α имеет структуру DivisionCommMonoid, расширяющую аддитивную структуру; операция деления определена как x / y, инверсия как x^{-1}.
LaTeX
$$$ \text{DivisionCommMonoid}(\text{Interval}(\alpha)) $$$
Lean4
@[to_additive existing NonemptyInterval.subtractionCommMonoid]
instance divisionCommMonoid : DivisionCommMonoid (NonemptyInterval α) :=
{ NonemptyInterval.commMonoid with
inv := Inv.inv
div := (· / ·)
div_eq_mul_inv := fun s t => by refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;> exact div_eq_mul_inv _ _
inv_inv := fun s => by apply NonemptyInterval.ext; exact inv_inv _
mul_inv_rev := fun s t => by refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;> exact mul_inv_rev _ _
inv_eq_of_mul := fun s t h =>
by
obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
rw [inv_pure, inv_eq_of_mul_eq_one_right hab] }
