unit_inv

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.unit_inv

English

For every IsUnit a, the inverse unit of a matches the unit information.

Русский

Для каждого IsUnit a обратная единица совпадает с единицей информации о a.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {a} (h : IsUnit a), IsUnit.inv h.unit = h.unit^{-1}$$$

Lean4

@[to_additive]
theorem unit_inv (h : IsUnit a) : h.inv.unit = h.unit⁻¹ :=
  Units.ext h.unit.val_inv_eq_inv_val.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru