rename_rename — Mathlib

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]

Похожие утверждения