instDiv — Mathlib

English

Units α^× carry a division operation defined by u / v = u · v^{-1}.

Русский

Единицы α^× образуют структуру деления, где операция деления задана как u / v = u · v^{-1}.

LaTeX

$$$\forall u,v \in \alpha^{\times},\ u/v = u\cdot v^{-1}$$$

Lean4

/-- Units of a monoid have division -/
@[to_additive /-- Additive units of an additive monoid have subtraction. -/
    ]
instance : Div αˣ where
  div := fun a b ↦
    { val := a * b⁻¹
      inv := b * a⁻¹
      val_inv := by rw [mul_assoc, inv_mul_cancel_left, mul_inv]
      inv_val := by rw [mul_assoc, inv_mul_cancel_left, mul_inv] }

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