liftRight_inv_mul

Mathlib.Algebra.Group.Units.Hom

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

← MathLib Explorer

English

Similarly, the left-inverse form holds: (liftRight f h x)⁻¹ · f x = 1.

Русский

Аналогично выполняется левая форма: (liftRight f h x)⁻¹ · f x = 1.

LaTeX

$$$(\\operatorname{liftRight} f g h\\, x)^{-1} \\cdot f(x) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem liftRight_inv_mul (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) : ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1 :=
  Units.liftRight_inv_mul (by intro; rfl) x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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