inv

Mathlib.Algebra.Group.Units.Defs

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

English

If a is a unit in a DivisionMonoid, then a^{-1} is also a unit.

Русский

Если a единица в делимом моноиде, то обратное к a также единица.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {a} (ha : IsUnit a), IsUnit a^{-1}$$$

Lean4

@[to_additive]
theorem inv (h : IsUnit a) : IsUnit a⁻¹ := by
  obtain ⟨u, hu⟩ := h
  rw [← hu, ← Units.val_inv_eq_inv_val]
  exact Units.isUnit _

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

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

Разделы

Аффилиация

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