Equivalences between polynomial rings #
This file establishes a number of equivalences between polynomial rings, based on equivalences between the underlying types.
Notation #
As in other polynomial files, we typically use the notation:
σ : Type*(indexing the variables)R : Type*[CommSemiring R](the coefficients)s : σ →₀ ℕ, a function fromσtoℕwhich is zero away from a finite set. This will give rise to a monomial inMvPolynomial σ Rwhich mathematicians might callX^sa : Ri : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : MvPolynomial σ R
Tags #
equivalence, isomorphism, morphism, ring hom, hom
The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
theorem
MvPolynomial.pUnitAlgEquiv_apply
(R : Type u)
[CommSemiring R]
(p : MvPolynomial PUnit.{u_2 + 1} R)
:
theorem
MvPolynomial.pUnitAlgEquiv_monomial
(R : Type u)
[CommSemiring R]
{d : PUnit.{1} →₀ ℕ}
{r : R}
:
theorem
MvPolynomial.pUnitAlgEquiv_symm_monomial
(R : Type u)
[CommSemiring R]
{d : PUnit.{1} →₀ ℕ}
{r : R}
:
def
MvPolynomial.mapEquiv
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[CommSemiring S₁]
[CommSemiring S₂]
(e : S₁ ≃+* S₂)
:
If e : A ≃+* B is an isomorphism of rings, then so is map e.
Equations
- MvPolynomial.mapEquiv σ e = { toFun := ⇑(MvPolynomial.map ↑e), invFun := ⇑(MvPolynomial.map ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
@[simp]
theorem
MvPolynomial.mapEquiv_apply
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[CommSemiring S₁]
[CommSemiring S₂]
(e : S₁ ≃+* S₂)
(a : MvPolynomial σ S₁)
:
@[simp]
@[simp]
theorem
MvPolynomial.mapEquiv_symm
{S₁ : Type v}
{S₂ : Type w}
(σ : Type u_1)
[CommSemiring S₁]
[CommSemiring S₂]
(e : S₁ ≃+* S₂)
:
@[simp]
theorem
MvPolynomial.mapEquiv_trans
{S₁ : Type v}
{S₂ : Type w}
{S₃ : Type x}
(σ : Type u_1)
[CommSemiring S₁]
[CommSemiring S₂]
[CommSemiring S₃]
(e : S₁ ≃+* S₂)
(f : S₂ ≃+* S₃)
:
def
MvPolynomial.mapAlgEquiv
{R : Type u}
(σ : Type u_1)
[CommSemiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[CommSemiring A₁]
[CommSemiring A₂]
[Algebra R A₁]
[Algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
:
If e : A ≃ₐ[R] B is an isomorphism of R-algebras, then so is map e.
Equations
- MvPolynomial.mapAlgEquiv σ e = { toFun := ⇑(MvPolynomial.map ↑e), invFun := (MvPolynomial.mapEquiv σ ↑e).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
@[simp]
theorem
MvPolynomial.mapAlgEquiv_apply
{R : Type u}
(σ : Type u_1)
[CommSemiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[CommSemiring A₁]
[CommSemiring A₂]
[Algebra R A₁]
[Algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
(a : MvPolynomial σ A₁)
:
@[simp]
theorem
MvPolynomial.mapAlgEquiv_refl
{R : Type u}
(σ : Type u_1)
[CommSemiring R]
{A₁ : Type u_2}
[CommSemiring A₁]
[Algebra R A₁]
:
@[simp]
theorem
MvPolynomial.mapAlgEquiv_symm
{R : Type u}
(σ : Type u_1)
[CommSemiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
[CommSemiring A₁]
[CommSemiring A₂]
[Algebra R A₁]
[Algebra R A₂]
(e : A₁ ≃ₐ[R] A₂)
:
@[simp]
theorem
MvPolynomial.mapAlgEquiv_trans
{R : Type u}
(σ : Type u_1)
[CommSemiring R]
{A₁ : Type u_2}
{A₂ : Type u_3}
{A₃ : Type u_4}
[CommSemiring A₁]
[CommSemiring A₂]
[CommSemiring A₃]
[Algebra R A₁]
[Algebra R A₂]
[Algebra R A₃]
(e : A₁ ≃ₐ[R] A₂)
(f : A₂ ≃ₐ[R] A₃)
:
theorem
MvPolynomial.eval₂_pUnitAlgEquiv_symm
{R : Type u_2}
{S : Type u_3}
[CommSemiring R]
[CommSemiring S]
{f : Polynomial R}
{φ : R →+* S}
{a : Unit → S}
:
theorem
MvPolynomial.eval₂_const_pUnitAlgEquiv_symm
{R : Type u_2}
{S : Type u_3}
[CommSemiring R]
[CommSemiring S]
{f : Polynomial R}
{φ : R →+* S}
{a : S}
:
theorem
MvPolynomial.eval₂_pUnitAlgEquiv
{R : Type u_2}
{S : Type u_3}
[CommSemiring R]
[CommSemiring S]
{f : MvPolynomial PUnit.{u_4 + 1} R}
{φ : R →+* S}
{a : PUnit.{u_4 + 1} → S}
:
theorem
MvPolynomial.eval₂_const_pUnitAlgEquiv
{R : Type u_2}
{S : Type u_3}
[CommSemiring R]
[CommSemiring S]
{f : MvPolynomial PUnit.{u_4 + 1} R}
{φ : R →+* S}
{a : S}
:
The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.
See sumRingEquiv for the ring isomorphism.
Equations
- MvPolynomial.sumToIter R S₁ S₂ = MvPolynomial.eval₂Hom (MvPolynomial.C.comp MvPolynomial.C) fun (bc : S₁ ⊕ S₂) => Sum.recOn bc MvPolynomial.X (⇑MvPolynomial.C ∘ MvPolynomial.X)
The function from multivariable polynomials in one type, with coefficients in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.
See sumRingEquiv for the ring isomorphism.
Equations
The algebra isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
- MvPolynomial.isEmptyAlgEquiv R σ = AlgEquiv.ofAlgHom (MvPolynomial.aeval fun (a : σ) => isEmptyElim a) (Algebra.ofId R (MvPolynomial σ R)) ⋯ ⋯
@[simp]
theorem
MvPolynomial.isEmptyAlgEquiv_apply
(R : Type u)
(σ : Type u_1)
[CommSemiring R]
[IsEmpty σ]
(a : MvPolynomial σ R)
:
@[simp]
theorem
MvPolynomial.aeval_injective_iff_of_isEmpty
{R : Type u}
{S₁ : Type v}
{σ : Type u_1}
[CommSemiring R]
[IsEmpty σ]
[CommSemiring S₁]
[Algebra R S₁]
{f : σ → S₁}
:
The ring isomorphism between multivariable polynomials in no variables and the ground ring.
Equations
@[simp]
theorem
MvPolynomial.isEmptyRingEquiv_apply
(R : Type u)
(σ : Type u_1)
[CommSemiring R]
[IsEmpty σ]
(a : MvPolynomial σ R)
:
theorem
MvPolynomial.isEmptyRingEquiv_symm_toRingHom
(R : Type u)
{σ : Type u_1}
[CommSemiring R]
[IsEmpty σ]
:
@[simp]
theorem
MvPolynomial.isEmptyRingEquiv_symm_apply
(R : Type u)
{σ : Type u_1}
[CommSemiring R]
[IsEmpty σ]
(r : R)
:
theorem
MvPolynomial.isEmptyRingEquiv_eq_coeff_zero
{σ : Type u_2}
{R : Type u_3}
[CommSemiring R]
[IsEmpty σ]
{x : MvPolynomial σ R}
:
def
MvPolynomial.mvPolynomialEquivMvPolynomial
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
(S₃ : Type x)
[CommSemiring R]
[CommSemiring S₃]
(f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃)
(g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
(hfgC : (f.comp g).comp C = C)
(hfgX : ∀ (n : S₂), f (g (X n)) = X n)
(hgfC : (g.comp f).comp C = C)
(hgfX : ∀ (n : S₁), g (f (X n)) = X n)
:
A helper function for sumRingEquiv.
Equations
- MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
@[simp]
theorem
MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
(S₃ : Type x)
[CommSemiring R]
[CommSemiring S₃]
(f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃)
(g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
(hfgC : (f.comp g).comp C = C)
(hfgX : ∀ (n : S₂), f (g (X n)) = X n)
(hgfC : (g.comp f).comp C = C)
(hgfX : ∀ (n : S₁), g (f (X n)) = X n)
(a : MvPolynomial S₂ S₃)
:
@[simp]
theorem
MvPolynomial.mvPolynomialEquivMvPolynomial_apply
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
(S₃ : Type x)
[CommSemiring R]
[CommSemiring S₃]
(f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃)
(g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
(hfgC : (f.comp g).comp C = C)
(hfgX : ∀ (n : S₂), f (g (X n)) = X n)
(hgfC : (g.comp f).comp C = C)
(hgfX : ∀ (n : S₁), g (f (X n)) = X n)
(a : MvPolynomial S₁ R)
:
The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.
Equations
- MvPolynomial.sumRingEquiv R S₁ S₂ = MvPolynomial.mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) S₁ (MvPolynomial S₂ R) (MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.iterToSum R S₁ S₂) ⋯ ⋯ ⋯ ⋯
The algebra isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.
Equations
- MvPolynomial.sumAlgEquiv R S₁ S₂ = { toEquiv := (MvPolynomial.sumRingEquiv R S₁ S₂).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
@[simp]
theorem
MvPolynomial.sumAlgEquiv_apply
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
[CommSemiring R]
(a : MvPolynomial (S₁ ⊕ S₂) R)
:
@[simp]
theorem
MvPolynomial.sumAlgEquiv_symm_apply
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
[CommSemiring R]
(a : MvPolynomial S₁ (MvPolynomial S₂ R))
:
theorem
MvPolynomial.sumAlgEquiv_comp_rename_inr
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
[CommSemiring R]
:
(↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr) = IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))
theorem
MvPolynomial.sumAlgEquiv_comp_rename_inl
(R : Type u)
(S₁ : Type v)
(S₂ : Type w)
[CommSemiring R]
:
noncomputable def
MvPolynomial.commAlgEquiv
(R : Type u_2)
(S₁ : Type u_3)
(S₂ : Type u_4)
[CommSemiring R]
:
The algebra isomorphism between multivariable polynomials in variables S₁ of multivariable
polynomials in variables S₂ and multivariable polynomials in variables S₂ of multivariable
polynomials in variables S₁.
Equations
- MvPolynomial.commAlgEquiv R S₁ S₂ = (MvPolynomial.sumAlgEquiv R S₁ S₂).symm.trans ((MvPolynomial.renameEquiv R (Equiv.sumComm S₁ S₂)).trans (MvPolynomial.sumAlgEquiv R S₂ S₁))
@[simp]
theorem
MvPolynomial.commAlgEquiv_C
{R : Type u_2}
{S₁ : Type u_3}
{S₂ : Type u_4}
[CommSemiring R]
(p : MvPolynomial S₂ R)
:
theorem
MvPolynomial.commAlgEquiv_C_X
{R : Type u_2}
{S₁ : Type u_3}
{S₂ : Type u_4}
[CommSemiring R]
(i : S₂)
:
@[simp]
theorem
MvPolynomial.commAlgEquiv_X
{R : Type u_2}
{S₁ : Type u_3}
{S₂ : Type u_4}
[CommSemiring R]
(i : S₁)
:
The algebra isomorphism between multivariable polynomials in Option S₁ and
polynomials with coefficients in MvPolynomial S₁ R.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
MvPolynomial.optionEquivLeft_symm_apply
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(a : Polynomial (MvPolynomial S₁ R))
:
@[simp]
theorem
MvPolynomial.optionEquivLeft_apply
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(a : MvPolynomial (Option S₁) R)
:
(optionEquivLeft R S₁) a = (aeval fun (o : Option S₁) => o.elim Polynomial.X fun (s : S₁) => Polynomial.C (X s)) a
theorem
MvPolynomial.optionEquivLeft_monomial
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(m : Option S₁ →₀ ℕ)
(r : R)
:
theorem
MvPolynomial.optionEquivLeft_coeff_coeff
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(n : Option S₁ →₀ ℕ)
(f : MvPolynomial (Option S₁) R)
:
The coefficient of n.some in the n none-th coefficient of optionEquivLeft R S₁ f
equals the coefficient of n in f
theorem
MvPolynomial.optionEquivLeft_elim_eval
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(s : S₁ → R)
(y : R)
(f : MvPolynomial (Option S₁) R)
:
(eval fun (x : Option S₁) => x.elim y s) f = Polynomial.eval y (Polynomial.map (eval s) ((optionEquivLeft R S₁) f))
The algebra isomorphism between multivariable polynomials in Option S₁ and
multivariable polynomials with coefficients in polynomials.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
MvPolynomial.optionEquivRight_symm_apply
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(a : MvPolynomial S₁ (Polynomial R))
:
(optionEquivRight R S₁).symm a = (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) => X (some i)) a
@[simp]
theorem
MvPolynomial.optionEquivRight_apply
(R : Type u)
(S₁ : Type v)
[CommSemiring R]
(a : MvPolynomial (Option S₁) R)
:
The algebra isomorphism between multivariable polynomials in Fin (n + 1) and
polynomials over multivariable polynomials in Fin n.
Equations
- MvPolynomial.finSuccEquiv R n = (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivLeft R (Fin n))
theorem
MvPolynomial.finSuccEquiv_eq
(R : Type u)
[CommSemiring R]
(n : ℕ)
:
↑(finSuccEquiv R n) = eval₂Hom (Polynomial.C.comp C) fun (i : Fin (n + 1)) =>
Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C (X k)) i
theorem
MvPolynomial.finSuccEquiv_apply
(R : Type u)
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial (Fin (n + 1)) R)
:
(finSuccEquiv R n) p = (eval₂Hom (Polynomial.C.comp C) fun (i : Fin (n + 1)) =>
Fin.cases Polynomial.X (fun (k : Fin n) => Polynomial.C (X k)) i)
p
theorem
MvPolynomial.finSuccEquiv_coeff_coeff
{R : Type u}
[CommSemiring R]
{n : ℕ}
(m : Fin n →₀ ℕ)
(f : MvPolynomial (Fin (n + 1)) R)
(i : ℕ)
:
The coefficient of m in the i-th coefficient of finSuccEquiv R n f equals the
coefficient of Finsupp.cons i m in f.
theorem
MvPolynomial.eval_eq_eval_mv_eval'
{R : Type u}
[CommSemiring R]
{n : ℕ}
(s : Fin n → R)
(y : R)
(f : MvPolynomial (Fin (n + 1)) R)
:
theorem
MvPolynomial.coeff_eval_eq_eval_coeff
{R : Type u}
(S₁ : Type v)
[CommSemiring R]
(s' : S₁ → R)
(f : Polynomial (MvPolynomial S₁ R))
(i : ℕ)
:
theorem
MvPolynomial.support_coeff_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{i : ℕ}
{m : Fin n →₀ ℕ}
:
theorem
MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le
{R : Type u}
[CommSemiring R]
{n : ℕ}
(f : MvPolynomial (Fin (n + 1)) R)
(i : ℕ)
(hi : ((finSuccEquiv R n) f).coeff i ≠ 0)
:
The totalDegree of a multivariable polynomial p is at least i more than the totalDegree of
the ith coefficient of finSuccEquiv applied to p, if this is nonzero.
theorem
MvPolynomial.support_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
(f : MvPolynomial (Fin (n + 1)) R)
:
@[deprecated MvPolynomial.support_finSuccEquiv (since := "2024-11-05")]
theorem
MvPolynomial.finSuccEquiv_support
{R : Type u}
[CommSemiring R]
{n : ℕ}
(f : MvPolynomial (Fin (n + 1)) R)
:
Alias of MvPolynomial.support_finSuccEquiv.
theorem
MvPolynomial.mem_support_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{x : ℕ}
:
theorem
MvPolynomial.image_support_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{i : ℕ}
:
@[deprecated MvPolynomial.image_support_finSuccEquiv (since := "2024-11-05")]
theorem
MvPolynomial.finSuccEquiv_support'
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{i : ℕ}
:
Alias of MvPolynomial.image_support_finSuccEquiv.
theorem
MvPolynomial.mem_image_support_coeff_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{i : ℕ}
{x : Fin (n + 1) →₀ ℕ}
:
theorem
MvPolynomial.mem_support_coeff_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
{i : ℕ}
{x : Fin n →₀ ℕ}
:
theorem
MvPolynomial.support_finSuccEquiv_nonempty
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
(h : f ≠ 0)
:
((finSuccEquiv R n) f).support.Nonempty
theorem
MvPolynomial.degree_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
{f : MvPolynomial (Fin (n + 1)) R}
(h : f ≠ 0)
:
theorem
MvPolynomial.natDegree_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
(f : MvPolynomial (Fin (n + 1)) R)
:
theorem
MvPolynomial.degreeOf_coeff_finSuccEquiv
{R : Type u}
[CommSemiring R]
{n : ℕ}
(p : MvPolynomial (Fin (n + 1)) R)
(j : Fin n)
(i : ℕ)
:
theorem
MvPolynomial.finSuccEquiv_rename_finSuccEquiv
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{n : ℕ}
(e : σ ≃ Fin n)
(φ : MvPolynomial (Option σ) R)
:
(finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) = Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)
Consider a multivariate polynomial φ whose variables are indexed by Option σ,
and suppose that σ ≃ Fin n.
Then one may view φ as a polynomial over MvPolynomial (Fin n) R, by
- renaming the variables via
Option σ ≃ Fin (n+1), and then singling out the0-th variable viaMvPolynomial.finSuccEquiv; - first viewing it as polynomial over
MvPolynomial σ RviaMvPolynomial.optionEquivLeft, and then renaming the variables.
This lemma shows that both constructions are the same.
@[simp]
theorem
MvPolynomial.rename_polynomial_aeval_X
(R : Type u)
[CommSemiring R]
{σ : Type u_2}
{τ : Type u_3}
(f : σ → τ)
(i : σ)
(p : Polynomial R)
:
noncomputable def
Polynomial.toMvPolynomial
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(i : σ)
:
The embedding of R[X] into R[Xᵢ] as an R-algebra homomorphism.
Equations
@[simp]
theorem
Polynomial.toMvPolynomial_C
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(i : σ)
(r : R)
:
@[simp]
theorem
Polynomial.toMvPolynomial_eq_rename_comp
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(i : σ)
:
toMvPolynomial i = (MvPolynomial.rename fun (x : Unit) => i).comp ↑(MvPolynomial.pUnitAlgEquiv R).symm
theorem
Polynomial.toMvPolynomial_injective
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(i : σ)
:
@[simp]
theorem
MvPolynomial.eval_comp_toMvPolynomial
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(f : σ → R)
(i : σ)
:
@[simp]
theorem
MvPolynomial.eval_toMvPolynomial
{R : Type u_1}
{σ : Type u_3}
[CommSemiring R]
(f : σ → R)
(i : σ)
(p : Polynomial R)
:
@[simp]
theorem
MvPolynomial.aeval_comp_toMvPolynomial
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(f : σ → S)
(i : σ)
:
@[simp]
theorem
MvPolynomial.aeval_toMvPolynomial
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
[CommSemiring R]
[CommSemiring S]
[Algebra R S]
(f : σ → S)
(i : σ)
(p : Polynomial R)
:
@[simp]
theorem
MvPolynomial.rename_comp_toMvPolynomial
{R : Type u_1}
{σ : Type u_3}
{τ : Type u_4}
[CommSemiring R]
(f : σ → τ)
(a : σ)
:
@[simp]
theorem
MvPolynomial.rename_toMvPolynomial
{R : Type u_1}
{σ : Type u_3}
{τ : Type u_4}
[CommSemiring R]
(f : σ → τ)
(a : σ)
(p : Polynomial R)
: