English
If f is a right inverse of g (g ∘ f = id), then map f is a right inverse of map g.
Русский
Если f — правый обратный к g (g ∘ f = id), то map f является правым обратным к map g.
LaTeX
$$$$\text{If } g \circ f = \mathrm{id}, \quad \operatorname{map} f \;\bigl(\operatorname{map} g\; p\bigr) = p.$$$$
Lean4
theorem coeff_map (p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p) := by
classical
apply MvPolynomial.induction_on p <;> clear p
· intro r m
simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
· intro p q hp hq m
simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
· intro p i hp m
simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]
