liftRight_inv_mul — Mathlib

English

With the same setup as above, the inverse of liftRight f g h x, when multiplied on the left with f x, yields the identity: (liftRight f g h x)⁻¹ · f x = 1.

Русский

При той же предпосылке, что и выше, обратное liftRight f g h x слева от f x даёт единицу: (liftRight f g h x)⁻¹ · f x = 1.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem liftRight_inv_mul {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) : ↑(liftRight f g h x)⁻¹ * f x = 1 := by
  rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

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