English
If f is a left inverse of g (f ∘ g = id), then map f is a left inverse of map g.
Русский
Если f — левый обратный к g (f ∘ g = id), то map f является левым обратным к map g.
LaTeX
$$$$\text{If } f \circ g = \mathrm{id}, \quad \operatorname{map} f \;\bigl(\operatorname{map} g\; p\bigr) = p.$$$$
Lean4
theorem map_eval₂ (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R) :
map f (eval₂ C g p) = eval₂ C (map f ∘ g) (map f p) :=
by
apply MvPolynomial.induction_on p
· intro r
rw [eval₂_C, map_C, map_C, eval₂_C]
· intro p q hp hq
rw [eval₂_add, (map f).map_add, hp, hq, (map f).map_add, eval₂_add]
· intro p s hp
rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X, comp_apply]
