Theorems · Definition · commutative algebra
Polynomial.toMvPolynomial
{R : Type u_1} → {σ : Type u_3} → [inst : CommSemiring R] → σ → Polynomial R →ₐ[R] MvPolynomial σ RThe embedding of R[X] into R[Xᵢ] as an R-algebra homomorphism.
- Defined in
- Mathlib.Algebra.MvPolynomial.Equiv
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement · cited by 5,681
- Finsuppstatement · cited by 5,255
- AlgHomstatement · cited by 3,236
- MvPolynomialstatement · cited by 2,140
- Polynomial.aevalproof · cited by 615
- MvPolynomial.Xproof · cited by 552
Cited by11
Results whose statement or proof uses this declaration.
- Polynomial.toMvPolynomial_Xstatement · cited by 4
- Polynomial.toMvPolynomial_Cstatement · cited by 1
- MvPolynomial.rename_comp_toMvPolynomialstatement and proof · cited by 1
- Polynomial.toMvPolynomial_eq_rename_compstatement and proof · cited by 1
- Polynomial.toMvPolynomial_injectivestatement · cited by 1
- MvPolynomial.aeval_comp_toMvPolynomialstatement · cited by 1
- MvPolynomial.eval_comp_toMvPolynomialstatement · cited by 1
- MvPolynomial.aeval_toMvPolynomialstatement · cited by 0
- Polynomial.toMvPolynomial_injstatement and proof · cited by 0
- MvPolynomial.eval_toMvPolynomialstatement · cited by 0
- MvPolynomial.rename_toMvPolynomialstatement · cited by 0