Theorems · Theorem · commutative algebra

MvPolynomial.map_rightInverse

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

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

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring