val_inv_mul

Mathlib.Algebra.Group.Units.Defs

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

English

For a unit a with unit u, a multiplied by the inverse of u equals 1.

Русский

Для единицы a произведение на обратное к её единице равно 1.

LaTeX

$$$\forall {M} [Monoid M] {a} (h : IsUnit a), a \cdot ↑h.unit^{-1} = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem val_inv_mul (h : IsUnit a) : ↑h.unit⁻¹ * a = 1 :=
  Units.mul_inv _

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

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

Разделы

Аффилиация

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