toAdd_div — Mathlib

English

The division of multiplicative elements corresponds to subtraction of their additive images: (x / y).toAdd = x.toAdd − y.toAdd.

Русский

Деление элементов в умножительной копии соответствует вычитанию их аддитивных изображений: (x / y).toAdd = x.toAdd − y.toAdd.

LaTeX

$$(x / y).toAdd = x.toAdd - y.toAdd$$

Lean4

@[simp]
theorem toAdd_div [Sub α] (x y : Multiplicative α) : (x / y).toAdd = x.toAdd - y.toAdd :=
  rfl

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