mathlib documentation

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

Notation

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

def mv_polynomial.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] :
(σ → τ)(mv_polynomial σ R →ₐ[R] mv_polynomial τ R)

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} [comm_semiring R] (f : σ → τ) (r : R) :

@[simp]
theorem mv_polynomial.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (i : σ) :

theorem mv_polynomial.map_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (f : R →+* S) (g : σ → τ) (p : mv_polynomial σ R) :

@[simp]
theorem mv_polynomial.rename_rename {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [comm_semiring R] (f : σ → τ) (g : τ → α) (p : mv_polynomial σ R) :

@[simp]
theorem mv_polynomial.rename_id {σ : Type u_1} {R : Type u_4} [comm_semiring R] (p : mv_polynomial σ R) :

theorem mv_polynomial.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (d : σ →₀ ) (r : R) :

theorem mv_polynomial.rename_eq {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (p : mv_polynomial σ R) :

theorem mv_polynomial.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) :

theorem mv_polynomial.eval₂_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : mv_polynomial σ R) :

theorem mv_polynomial.eval₂_hom_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (f : R →+* S) (k : σ → τ) (g : τ → S) (p : mv_polynomial σ R) :

theorem mv_polynomial.aeval_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (k : σ → τ) (g : τ → S) (p : mv_polynomial σ R) [algebra R S] :

theorem mv_polynomial.rename_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (k : σ → τ) (p : mv_polynomial σ R) (g : τ → mv_polynomial σ R) :

theorem mv_polynomial.rename_prodmk_eval₂ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (p : mv_polynomial σ R) (j : τ) (g : σ → mv_polynomial σ R) :

theorem mv_polynomial.eval₂_rename_prodmk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [comm_semiring R] [comm_semiring S] (f : R →+* S) (g : σ × τ → S) (i : σ) (p : mv_polynomial τ R) :

theorem mv_polynomial.eval_rename_prodmk {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (g : σ × τ → R) (i : σ) (p : mv_polynomial τ R) :

theorem mv_polynomial.exists_finset_rename {σ : Type u_1} {R : Type u_4} [comm_semiring R] (p : mv_polynomial σ R) :
∃ (s : finset σ) (q : mv_polynomial {x // x s} R), p = (mv_polynomial.rename coe) q

Every polynomial is a polynomial in finitely many variables.

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

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} [comm_semiring R] (f : σ → τ) (c : →+* R) (g : τ → R) (p : mv_polynomial σ ) :

@[simp]
theorem mv_polynomial.coeff_rename_map_domain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (hf : function.injective f) (φ : mv_polynomial σ R) (d : σ →₀ ) :

theorem mv_polynomial.coeff_rename_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →₀ ) :

theorem mv_polynomial.coeff_rename_ne_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [comm_semiring R] (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →₀ ) :

@[simp]
theorem mv_polynomial.constant_coeff_rename {σ : Type u_1} {R : Type u_4} [comm_semiring R] {τ : Type u_2} (f : σ → τ) (φ : mv_polynomial σ R) :