map_rightInverse — Mathlib

English

If f is a right inverse of g, then map f is a right inverse of map g (repeat).

Русский

Если f — правый обратный к g, то map f — правый обратный к map g (повтор).

LaTeX

$$$$\text{If } g \circ f = \mathrm{id}, \ \operatorname{map} f \;\bigl(\operatorname{map} g\; p\bigr) = p.$$$$

Lean4

/-- If `f` is a right-inverse of `g` then `map f` is a right-inverse of `map g`. -/
theorem map_rightInverse {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse f g) :
    Function.RightInverse (map f : MvPolynomial σ R → MvPolynomial σ S₁) (map g) :=
  (map_leftInverse hf.leftInverse).rightInverse

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