Theorems · Definition · commutative algebra
MvPolynomial.mapEquivMonic
(R : Type u_1) →
(S : Type u_2) →
[inst : CommRing R] →
[inst_1 : CommRing S] →
[inst_2 : Algebra R S] → (n : ℕ) → (MvPolynomial (Fin n) R →ₐ[R] S) ≃ Polynomial.MonicDegreeEq S nMonicDegreeEq · n is representable by R[X₁,...,Xₙ],
with the universal element being freeMonic.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Equivstatement · cited by 8,337
- Finsuppstatement · cited by 5,255
- AlgHomstatement and proof · cited by 3,236
- MvPolynomialstatement and proof · cited by 2,140
- Polynomial.coeffproof · cited by 1,045
- AlgHom.toRingHomproof · cited by 490
- MvPolynomial.aevalproof · cited by 298
- Polynomial.MonicDegreeEqstatement and proof · cited by 22
- Polynomial.MonicDegreeEq.mapproof · cited by 12
- Polynomial.MonicDegreeEq.freeMonicproof · cited by 4
Cited by12
Results whose statement or proof uses this declaration.
- MvPolynomial.universalFactorizationMapproof · cited by 19
- MvPolynomial.coe_mapEquivMonic_compstatement · cited by 2
- MvPolynomial.pderiv_inl_universalFactorizationMap_Xproof · cited by 1
- MvPolynomial.pderiv_inr_universalFactorizationMap_Xproof · cited by 1
- MvPolynomial.universalFactorizationMapLiftEquivstatement and proof · cited by 1
- MvPolynomial.mapEquivMonic_symm_mapstatement and proof · cited by 1
- MvPolynomial.universalFactorizationMap_freeMonicproof · cited by 1
- MvPolynomial.coe_mapEquivMonic_comp'statement · cited by 1
- Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMapstatement and proof · cited by 1
- Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'statement and proof · cited by 1
- Polynomial.UniversalFactorizationRing.jacobian_resentationproof · cited by 1
- MvPolynomial.mapEquivMonic_symm_map_algebraMapstatement and proof · cited by 0