val_inv

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#Units.Simps.val_inv

English

For a unit u, the value of its inverse equals the inverse value: val_inv(u) = u^{-1} in α.

Русский

Для единицы u, значение обратного равно обратному значению: val_inv(u) = u^{-1} в α.

LaTeX

$$$$ \\operatorname{val\\_inv}(u) = u^{-1}. $$$$

Lean4

/-- See Note [custom simps projection] -/
@[to_additive /-- See Note [custom simps projection] -/
    ]
def val_inv (u : αˣ) : α :=
  ↑(u⁻¹)

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

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

Разделы

Аффилиация

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