rename_leftInverse — Mathlib

English

If hf is a LeftInverse between f:σ→τ and g:τ→σ, then rename f has a left inverse rename g on polynomials.

Русский

Если hf является левым обратным к f:σ→τ и g:τ→σ, то rename f имеет левый обратный на полиномах, заданный rename g.

LaTeX

$$$\\text{LeftInverse}(\\text{rename}_f, \\text{rename}_g) \\quad\\text{whenever } hf: f \\circ g = \\mathrm{id}. $$$

Lean4

theorem rename_leftInverse {f : σ → τ} {g : τ → σ} (hf : Function.LeftInverse f g) :
    Function.LeftInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g) :=
  by
  intro x
  simp [hf.comp_eq_id]

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