data.mv_polynomial.equiv

source

noncomputable def mv_polynomial.punit_alg_equiv (R : Type u) [comm_semiring R] :

mv_polynomial punit R ≃ₐ[R] polynomial R

The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.

Equations

mv_polynomial.punit_alg_equiv R = {to_fun := mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X), inv_fun := polynomial.eval₂ mv_polynomial.C (mv_polynomial.X punit.star), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem mv_polynomial.punit_alg_equiv_apply (R : Type u) [comm_semiring R] (p : mv_polynomial punit R) :

⇑(mv_polynomial.punit_alg_equiv R) p = mv_polynomial.eval₂ polynomial.C (λ (u : punit), polynomial.X) p

source

@[simp]

theorem mv_polynomial.punit_alg_equiv_symm_apply (R : Type u) [comm_semiring R] (p : polynomial R) :

⇑((mv_polynomial.punit_alg_equiv R).symm) p = polynomial.eval₂ mv_polynomial.C (mv_polynomial.X punit.star) p

source

@[simp]

theorem mv_polynomial.map_equiv_apply {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] (e : S₁ ≃+* S₂) (ᾰ : mv_polynomial σ S₁) :

⇑(mv_polynomial.map_equiv σ e) ᾰ = ⇑(mv_polynomial.map ↑e) ᾰ

source

noncomputable def mv_polynomial.map_equiv {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] (e : S₁ ≃+* S₂) :

mv_polynomial σ S₁ ≃+* mv_polynomial σ S₂

If e : A ≃+* B is an isomorphism of rings, then so is map e.

Equations

mv_polynomial.map_equiv σ e = {to_fun := ⇑(mv_polynomial.map ↑e), inv_fun := ⇑(mv_polynomial.map ↑(e.symm)), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem mv_polynomial.map_equiv_refl {R : Type u} (σ : Type u_1) [comm_semiring R] :

mv_polynomial.map_equiv σ (ring_equiv.refl R) = ring_equiv.refl (mv_polynomial σ R)

source

@[simp]

theorem mv_polynomial.map_equiv_symm {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] (e : S₁ ≃+* S₂) :

(mv_polynomial.map_equiv σ e).symm = mv_polynomial.map_equiv σ e.symm

source

@[simp]

theorem mv_polynomial.map_equiv_trans {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [comm_semiring S₁] [comm_semiring S₂] [comm_semiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :

(mv_polynomial.map_equiv σ e).trans (mv_polynomial.map_equiv σ f) = mv_polynomial.map_equiv σ (e.trans f)

source

@[simp]

theorem mv_polynomial.map_alg_equiv_apply {R : Type u} (σ : Type u_1) [comm_semiring R] {A₁ : Type u_2} {A₂ : Type u_3} [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (ᾰ : mv_polynomial σ A₁) :

⇑(mv_polynomial.map_alg_equiv σ e) ᾰ = ⇑(mv_polynomial.map ↑e) ᾰ

source

noncomputable def mv_polynomial.map_alg_equiv {R : Type u} (σ : Type u_1) [comm_semiring R] {A₁ : Type u_2} {A₂ : Type u_3} [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

mv_polynomial σ A₁ ≃ₐ[R] mv_polynomial σ A₂

If e : A ≃ₐ[R] B is an isomorphism of R-algebras, then so is map e.

Equations

mv_polynomial.map_alg_equiv σ e = {to_fun := ⇑(mv_polynomial.map ↑e), inv_fun := (mv_polynomial.map_equiv σ ↑e).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem mv_polynomial.map_alg_equiv_refl {R : Type u} (σ : Type u_1) [comm_semiring R] {A₁ : Type u_2} [comm_semiring A₁] [algebra R A₁] :

mv_polynomial.map_alg_equiv σ alg_equiv.refl = alg_equiv.refl

source

@[simp]

theorem mv_polynomial.map_alg_equiv_symm {R : Type u} (σ : Type u_1) [comm_semiring R] {A₁ : Type u_2} {A₂ : Type u_3} [comm_semiring A₁] [comm_semiring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

(mv_polynomial.map_alg_equiv σ e).symm = mv_polynomial.map_alg_equiv σ e.symm

source

@[simp]

theorem mv_polynomial.map_alg_equiv_trans {R : Type u} (σ : Type u_1) [comm_semiring R] {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [comm_semiring A₁] [comm_semiring A₂] [comm_semiring A₃] [algebra R A₁] [algebra R A₂] [algebra R A₃] (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :

(mv_polynomial.map_alg_equiv σ e).trans (mv_polynomial.map_alg_equiv σ f) = mv_polynomial.map_alg_equiv σ (e.trans f)

source

noncomputable def mv_polynomial.sum_to_iter (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :

mv_polynomial (S₁ ⊕ S₂) R →+* mv_polynomial S₁ (mv_polynomial S₂ R)

The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.

See sum_ring_equiv for the ring isomorphism.

Equations

mv_polynomial.sum_to_iter R S₁ S₂ = mv_polynomial.eval₂_hom (mv_polynomial.C.comp mv_polynomial.C) (λ (bc : S₁ ⊕ S₂), bc.rec_on mv_polynomial.X (⇑mv_polynomial.C ∘ mv_polynomial.X))

source

@[simp]

theorem mv_polynomial.sum_to_iter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (a : R) :

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (⇑mv_polynomial.C a) = ⇑mv_polynomial.C (⇑mv_polynomial.C a)

source

@[simp]

theorem mv_polynomial.sum_to_iter_Xl (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (b : S₁) :

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.X (sum.inl b)) = mv_polynomial.X b

source

@[simp]

theorem mv_polynomial.sum_to_iter_Xr (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (c : S₂) :

⇑(mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.X (sum.inr c)) = ⇑mv_polynomial.C (mv_polynomial.X c)

source

noncomputable def mv_polynomial.iter_to_sum (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :

mv_polynomial S₁ (mv_polynomial S₂ R) →+* mv_polynomial (S₁ ⊕ S₂) R

The function from multivariable polynomials in one type, with coefficents in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.

See sum_ring_equiv for the ring isomorphism.

Equations

mv_polynomial.iter_to_sum R S₁ S₂ = mv_polynomial.eval₂_hom (mv_polynomial.eval₂_hom mv_polynomial.C (mv_polynomial.X ∘ sum.inr)) (mv_polynomial.X ∘ sum.inl)

source

theorem mv_polynomial.iter_to_sum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (a : R) :

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (⇑mv_polynomial.C (⇑mv_polynomial.C a)) = ⇑mv_polynomial.C a

source

theorem mv_polynomial.iter_to_sum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (b : S₁) :

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (mv_polynomial.X b) = mv_polynomial.X (sum.inl b)

source

theorem mv_polynomial.iter_to_sum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] (c : S₂) :

⇑(mv_polynomial.iter_to_sum R S₁ S₂) (⇑mv_polynomial.C (mv_polynomial.X c)) = mv_polynomial.X (sum.inr c)

source

@[simp]

theorem mv_polynomial.is_empty_alg_equiv_symm_apply_to_fun (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : R) (i : σ →₀ ℕ) :

⇑(⇑((mv_polynomial.is_empty_alg_equiv R σ).symm) ᾰ) i = pi.single 0 ᾰ i

source

@[simp]

theorem mv_polynomial.is_empty_alg_equiv_apply (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : mv_polynomial σ R) :

⇑(mv_polynomial.is_empty_alg_equiv R σ) ᾰ = ⇑(mv_polynomial.aeval he.elim) ᾰ

source

@[simp]

theorem mv_polynomial.is_empty_alg_equiv_symm_apply_support (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : R) :

(⇑((mv_polynomial.is_empty_alg_equiv R σ).symm) ᾰ).support = ite (ᾰ = 0) ∅ {0}

source

noncomputable def mv_polynomial.is_empty_alg_equiv (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] :

mv_polynomial σ R ≃ₐ[R] R

The algebra isomorphism between multivariable polynomials in no variables and the ground ring.

Equations

mv_polynomial.is_empty_alg_equiv R σ = alg_equiv.of_alg_hom (mv_polynomial.aeval he.elim) (algebra.of_id R (mv_polynomial σ R)) _ _

source

@[simp]

theorem mv_polynomial.is_empty_ring_equiv_symm_apply_support (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : R) :

(⇑((mv_polynomial.is_empty_ring_equiv R σ).symm) ᾰ).support = ite (ᾰ = 0) ∅ {0}

source

@[simp]

theorem mv_polynomial.is_empty_ring_equiv_symm_apply_to_fun (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : R) (i : σ →₀ ℕ) :

⇑(⇑((mv_polynomial.is_empty_ring_equiv R σ).symm) ᾰ) i = pi.single 0 ᾰ i

source

noncomputable def mv_polynomial.is_empty_ring_equiv (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] :

mv_polynomial σ R ≃+* R

The ring isomorphism between multivariable polynomials in no variables and the ground ring.

Equations

mv_polynomial.is_empty_ring_equiv R σ = (mv_polynomial.is_empty_alg_equiv R σ).to_ring_equiv

source

@[simp]

theorem mv_polynomial.is_empty_ring_equiv_apply (R : Type u) (σ : Type u_1) [comm_semiring R] [he : is_empty σ] (ᾰ : mv_polynomial σ R) :

⇑(mv_polynomial.is_empty_ring_equiv R σ) ᾰ = ⇑(mv_polynomial.aeval he.elim) ᾰ

source

@[simp]

theorem mv_polynomial.mv_polynomial_equiv_mv_polynomial_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : (f.comp g).comp mv_polynomial.C = mv_polynomial.C) (hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C) (hgfX : ∀ (n : S₁), ⇑g (⇑f (mv_polynomial.X n)) = mv_polynomial.X n) (ᾰ : mv_polynomial S₁ R) :

⇑(mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) ᾰ = ⇑f ᾰ

source

@[simp]

theorem mv_polynomial.mv_polynomial_equiv_mv_polynomial_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : (f.comp g).comp mv_polynomial.C = mv_polynomial.C) (hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C) (hgfX : ∀ (n : S₁), ⇑g (⇑f (mv_polynomial.X n)) = mv_polynomial.X n) (ᾰ : mv_polynomial S₂ S₃) :

⇑((mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX).symm) ᾰ = ⇑g ᾰ

source

noncomputable def mv_polynomial.mv_polynomial_equiv_mv_polynomial (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [comm_semiring R] [comm_semiring S₃] (f : mv_polynomial S₁ R →+* mv_polynomial S₂ S₃) (g : mv_polynomial S₂ S₃ →+* mv_polynomial S₁ R) (hfgC : (f.comp g).comp mv_polynomial.C = mv_polynomial.C) (hfgX : ∀ (n : S₂), ⇑f (⇑g (mv_polynomial.X n)) = mv_polynomial.X n) (hgfC : (g.comp f).comp mv_polynomial.C = mv_polynomial.C) (hgfX : ∀ (n : S₁), ⇑g (⇑f (mv_polynomial.X n)) = mv_polynomial.X n) :

mv_polynomial S₁ R ≃+* mv_polynomial S₂ S₃

A helper function for sum_ring_equiv.

Equations

mv_polynomial.mv_polynomial_equiv_mv_polynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX = {to_fun := ⇑f, inv_fun := ⇑g, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

noncomputable def mv_polynomial.sum_ring_equiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :

mv_polynomial (S₁ ⊕ S₂) R ≃+* mv_polynomial S₁ (mv_polynomial S₂ R)

The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.

Equations

mv_polynomial.sum_ring_equiv R S₁ S₂ = mv_polynomial.mv_polynomial_equiv_mv_polynomial R (S₁ ⊕ S₂) S₁ (mv_polynomial S₂ R) (mv_polynomial.sum_to_iter R S₁ S₂) (mv_polynomial.iter_to_sum R S₁ S₂) _ _ _ _

source

noncomputable def mv_polynomial.sum_alg_equiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [comm_semiring R] :

mv_polynomial (S₁ ⊕ S₂) R ≃ₐ[R] mv_polynomial S₁ (mv_polynomial S₂ R)

The algebra isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficents in multivariable polynomials in the other type.

Equations

mv_polynomial.sum_alg_equiv R S₁ S₂ = {to_fun := (mv_polynomial.sum_ring_equiv R S₁ S₂).to_fun, inv_fun := (mv_polynomial.sum_ring_equiv R S₁ S₂).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem mv_polynomial.option_equiv_left_apply (R : Type u) (S₁ : Type v) [comm_semiring R] (ᾰ : mv_polynomial (option S₁) R) :

⇑(mv_polynomial.option_equiv_left R S₁) ᾰ = ⇑(mv_polynomial.aeval (option.elim polynomial.X (λ (s : S₁), ⇑polynomial.C (mv_polynomial.X s)))) ᾰ

source

noncomputable def mv_polynomial.option_equiv_left (R : Type u) (S₁ : Type v) [comm_semiring R] :

mv_polynomial (option S₁) R ≃ₐ[R] polynomial (mv_polynomial S₁ R)

The algebra isomorphism between multivariable polynomials in option S₁ and polynomials with coefficients in mv_polynomial S₁ R.

Equations

mv_polynomial.option_equiv_left R S₁ = alg_equiv.of_alg_hom (mv_polynomial.aeval (λ (o : option S₁), option.elim polynomial.X (λ (s : S₁), ⇑polynomial.C (mv_polynomial.X s)) o)) (polynomial.aeval_tower (mv_polynomial.rename option.some) (mv_polynomial.X option.none)) _ _

source

@[simp]

theorem mv_polynomial.option_equiv_left_symm_apply (R : Type u) (S₁ : Type v) [comm_semiring R] (ᾰ : polynomial (mv_polynomial S₁ R)) :

⇑((mv_polynomial.option_equiv_left R S₁).symm) ᾰ = ⇑(polynomial.aeval_tower (mv_polynomial.rename option.some) (mv_polynomial.X option.none)) ᾰ

source

noncomputable def mv_polynomial.option_equiv_right (R : Type u) (S₁ : Type v) [comm_semiring R] :

mv_polynomial (option S₁) R ≃ₐ[R] mv_polynomial S₁ (polynomial R)

The algebra isomorphism between multivariable polynomials in option S₁ and multivariable polynomials with coefficients in polynomials.

Equations

mv_polynomial.option_equiv_right R S₁ = alg_equiv.of_alg_hom (mv_polynomial.aeval (λ (o : option S₁), option.elim (⇑mv_polynomial.C polynomial.X) mv_polynomial.X o)) (mv_polynomial.aeval_tower (polynomial.aeval (mv_polynomial.X option.none)) (λ (i : S₁), mv_polynomial.X (option.some i))) _ _

source

noncomputable def mv_polynomial.fin_succ_equiv (R : Type u) [comm_semiring R] (n : ℕ) :

mv_polynomial (fin (n + 1)) R ≃ₐ[R] polynomial (mv_polynomial (fin n) R)

The algebra isomorphism between multivariable polynomials in fin (n + 1) and polynomials over multivariable polynomials in fin n.

Equations

mv_polynomial.fin_succ_equiv R n = (mv_polynomial.rename_equiv R (fin_succ_equiv n)).trans (mv_polynomial.option_equiv_left R (fin n))

source

theorem mv_polynomial.fin_succ_equiv_eq (R : Type u) [comm_semiring R] (n : ℕ) :

↑(mv_polynomial.fin_succ_equiv R n) = mv_polynomial.eval₂_hom (polynomial.C.comp mv_polynomial.C) (λ (i : fin (n + 1)), fin.cases polynomial.X (λ (k : fin n), ⇑polynomial.C (mv_polynomial.X k)) i)

source

@[simp]

theorem mv_polynomial.fin_succ_equiv_apply (R : Type u) [comm_semiring R] (n : ℕ) (p : mv_polynomial (fin (n + 1)) R) :

⇑(mv_polynomial.fin_succ_equiv R n) p = ⇑(mv_polynomial.eval₂_hom (polynomial.C.comp mv_polynomial.C) (λ (i : fin (n + 1)), fin.cases polynomial.X (λ (k : fin n), ⇑polynomial.C (mv_polynomial.X k)) i)) p

source

theorem mv_polynomial.fin_succ_equiv_comp_C_eq_C {R : Type u} [comm_semiring R] (n : ℕ) :

↑((mv_polynomial.fin_succ_equiv R n).symm).comp (polynomial.C.comp mv_polynomial.C) = mv_polynomial.C

source

theorem mv_polynomial.fin_succ_equiv_X_zero {R : Type u} [comm_semiring R] {n : ℕ} :

⇑(mv_polynomial.fin_succ_equiv R n) (mv_polynomial.X 0) = polynomial.X

source

theorem mv_polynomial.fin_succ_equiv_X_succ {R : Type u} [comm_semiring R] {n : ℕ} {j : fin n} :

⇑(mv_polynomial.fin_succ_equiv R n) (mv_polynomial.X j.succ) = ⇑polynomial.C (mv_polynomial.X j)

source

theorem mv_polynomial.fin_succ_equiv_coeff_coeff {R : Type u} [comm_semiring R] {n : ℕ} (m : fin n →₀ ℕ) (f : mv_polynomial (fin (n + 1)) R) (i : ℕ) :

mv_polynomial.coeff m ((⇑(mv_polynomial.fin_succ_equiv R n) f).coeff i) = mv_polynomial.coeff (finsupp.cons i m) f

The coefficient of m in the i-th coefficient of fin_succ_equiv R n f equals the coefficient of finsupp.cons i m in f.

source

theorem mv_polynomial.eval_eq_eval_mv_eval' {R : Type u} [comm_semiring R] {n : ℕ} (s : fin n → R) (y : R) (f : mv_polynomial (fin (n + 1)) R) :

⇑(mv_polynomial.eval (fin.cons y s)) f = polynomial.eval y (polynomial.map (mv_polynomial.eval s) (⇑(mv_polynomial.fin_succ_equiv R n) f))

source

theorem mv_polynomial.coeff_eval_eq_eval_coeff {R : Type u} [comm_semiring R] {n : ℕ} (s' : fin n → R) (f : polynomial (mv_polynomial (fin n) R)) (i : ℕ) :

(polynomial.map (mv_polynomial.eval s') f).coeff i = ⇑(mv_polynomial.eval s') (f.coeff i)

source

theorem mv_polynomial.support_coeff_fin_succ_equiv {R : Type u} [comm_semiring R] {n : ℕ} {f : mv_polynomial (fin (n + 1)) R} {i : ℕ} {m : fin n →₀ ℕ} :

m ∈ ((⇑(mv_polynomial.fin_succ_equiv R n) f).coeff i).support ↔ finsupp.cons i m ∈ f.support

source

theorem mv_polynomial.fin_succ_equiv_support {R : Type u} [comm_semiring R] {n : ℕ} (f : mv_polynomial (fin (n + 1)) R) :

(⇑(mv_polynomial.fin_succ_equiv R n) f).support = finset.image (λ (m : fin (n + 1) →₀ ℕ), ⇑m 0) f.support

source

theorem mv_polynomial.fin_succ_equiv_support' {R : Type u} [comm_semiring R] {n : ℕ} {f : mv_polynomial (fin (n + 1)) R} {i : ℕ} :

finset.image (finsupp.cons i) ((⇑(mv_polynomial.fin_succ_equiv R n) f).coeff i).support = finset.filter (λ (m : fin (n + 1) →₀ ℕ), ⇑m 0 = i) f.support

source

theorem mv_polynomial.support_fin_succ_equiv_nonempty {R : Type u} [comm_semiring R] {n : ℕ} {f : mv_polynomial (fin (n + 1)) R} (h : f ≠ 0) :

(⇑(mv_polynomial.fin_succ_equiv R n) f).support.nonempty

source

theorem mv_polynomial.degree_fin_succ_equiv {R : Type u} [comm_semiring R] {n : ℕ} {f : mv_polynomial (fin (n + 1)) R} (h : f ≠ 0) :

(⇑(mv_polynomial.fin_succ_equiv R n) f).degree = ↑(mv_polynomial.degree_of 0 f)

source

theorem mv_polynomial.nat_degree_fin_succ_equiv {R : Type u} [comm_semiring R] {n : ℕ} (f : mv_polynomial (fin (n + 1)) R) :

(⇑(mv_polynomial.fin_succ_equiv R n) f).nat_degree = mv_polynomial.degree_of 0 f

source

theorem mv_polynomial.degree_of_coeff_fin_succ_equiv {R : Type u} [comm_semiring R] {n : ℕ} (p : mv_polynomial (fin (n + 1)) R) (j : fin n) (i : ℕ) :

mv_polynomial.degree_of j ((⇑(mv_polynomial.fin_succ_equiv R n) p).coeff i) ≤ mv_polynomial.degree_of j.succ p

mathlib documentation

Equivalences between polynomial rings #

Notation #

Tags #