Theorems · Theorem · commutative algebra

MvPolynomial.map_leftInverse

∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
  {g : S₁ →+* R}, Function.LeftInverse ⇑f ⇑g → Function.LeftInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)

If f is a left-inverse of g then map f is a left-inverse of map g.

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

1 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiring