mul_liftRight_inv — Mathlib

English

For a monoid hom f and hf, the product of f x with the inverse of liftRight f h x equals 1, equivalently f x · (liftRight f h x)⁻¹ = 1.

Русский

Пусть f и hf как выше; тогда f(x) умножить на обратное liftRight f h x даёт единицу: f(x) · (liftRight f h x)⁻¹ = 1.

LaTeX

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

Lean4

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

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