English
For f: σ → τ and g: τ → α, rename g ∘ rename f = rename (g ∘ f).
Русский
Для f: σ → τ и g: τ → α выполнено переименование: rename_g ∘ rename_f = rename_{g ∘ f}.
LaTeX
$$$\\text{rename } g \\circ \\text{rename } f = \\text{rename } (g \\circ f).$$$
Lean4
@[simp]
theorem rename_rename (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) : rename g (rename f p) = rename (g ∘ f) p :=
by
nth_rw 2 [rename]
simp_rw [aeval_def, algebraMap_eq, rename, aeval_eq_eval₂Hom]
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
simp only [comp_def, eval₂Hom_X']
refine eval₂Hom_congr ?_ rfl rfl
ext1; simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]