unit_div — Mathlib

English

If a and b are units, then the unit of a/b is the quotient of their units: (IsUnit a).unit divided by (IsUnit b).unit

Русский

Если a и b единицы, то единица a/b равна частному их единиц.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {a\,b : \alpha} (ha : IsUnit a) (hb : IsUnit b), IsUnit a \div IsUnit b = ?$$$

Lean4

@[to_additive]
theorem unit_div (ha : IsUnit a) (hb : IsUnit b) : (ha.div hb).unit = ha.unit / hb.unit :=
  Units.ext (ha.unit.val_div_eq_div_val hb.unit).symm

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