# mathlibdocumentation

data.mv_polynomial.rename

# Renaming variables of polynomials #

This file establishes the rename operation on multivariate polynomials, which modifies the set of variables.

## Main declarations #

• mv_polynomial.rename
• mv_polynomial.rename_equiv

## Notation #

As in other polynomial files, we typically use the notation:

• σ τ α : Type* (indexing the variables)

• R S : Type* [comm_semiring R] [comm_semiring S] (the coefficients)

• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s

• r : R elements of the coefficient ring

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• p : mv_polynomial σ α

def mv_polynomial.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) :

Rename all the variables in a multivariable polynomial.

Equations
@[simp]
theorem mv_polynomial.rename_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (r : R) :
@[simp]
theorem mv_polynomial.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (i : σ) :
theorem mv_polynomial.map_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : R →+* S) (g : σ → τ) (p : R) :
p) = ( p)
@[simp]
theorem mv_polynomial.rename_rename {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → α) (p : R) :
@[simp]
theorem mv_polynomial.rename_id {σ : Type u_1} {R : Type u_4} (p : R) :
= p
theorem mv_polynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (d : σ →₀ ) (r : R) :
theorem mv_polynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (p : R) :
theorem mv_polynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (hf : function.injective f) :
@[simp]
theorem mv_polynomial.rename_equiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) (f : σ τ) (ᾰ : R) :
=
def mv_polynomial.rename_equiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) (f : σ τ) :

mv_polynomial.rename e is an equivalence when e is.

Equations
@[simp]
theorem mv_polynomial.rename_equiv_refl {σ : Type u_1} (R : Type u_4)  :
@[simp]
theorem mv_polynomial.rename_equiv_symm {σ : Type u_1} {τ : Type u_2} (R : Type u_4) (f : σ τ) :
@[simp]
theorem mv_polynomial.rename_equiv_trans {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) (e : σ τ) (f : τ α) :
= (e.trans f)
theorem mv_polynomial.eval₂_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : R →+* S) (k : σ → τ) (g : τ → S) (p : R) :
p) = (g k) p
theorem mv_polynomial.eval₂_hom_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : R →+* S) (k : σ → τ) (g : τ → S) (p : R) :
p) = (g k)) p
theorem mv_polynomial.aeval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (k : σ → τ) (g : τ → S) (p : R) [ S] :
theorem mv_polynomial.rename_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (k : σ → τ) (p : R) (g : τ → ) :
p) =
theorem mv_polynomial.rename_prodmk_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (p : R) (j : τ) (g : σ → ) :
= (λ (x : σ), (g x)) p
theorem mv_polynomial.eval₂_rename_prodmk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : R →+* S) (g : σ × τ → S) (i : σ) (p : R) :
( p) = (λ (j : τ), g (i, j)) p
theorem mv_polynomial.eval_rename_prodmk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (g : σ × τ → R) (i : σ) (p : R) :
( p) = (mv_polynomial.eval (λ (j : τ), g (i, j))) p
theorem mv_polynomial.exists_finset_rename {σ : Type u_1} {R : Type u_4} (p : R) :
∃ (s : finset σ) (q : mv_polynomial {x // x s} R),

Every polynomial is a polynomial in finitely many variables.

theorem mv_polynomial.exists_fin_rename {σ : Type u_1} {R : Type u_4} (p : R) :
∃ (n : ) (f : fin n → σ) (hf : (q : mv_polynomial (fin n) R), p =

Every polynomial is a polynomial in finitely many variables.

theorem mv_polynomial.eval₂_cast_comp {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (c : →+* R) (g : τ → R) (p : ) :
(g f) p = p)
@[simp]
theorem mv_polynomial.coeff_rename_map_domain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (hf : function.injective f) (φ : R) (d : σ →₀ ) :
φ) =
theorem mv_polynomial.coeff_rename_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (φ : R) (d : τ →₀ ) (h : ∀ (u : σ →₀ ), = d = 0) :
φ) = 0
theorem mv_polynomial.coeff_rename_ne_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) (φ : R) (d : τ →₀ ) (h : φ) 0) :
∃ (u : σ →₀ ), = d 0
@[simp]
theorem mv_polynomial.constant_coeff_rename {σ : Type u_1} {R : Type u_4} {τ : Type u_2} (f : σ → τ) (φ : R) :