Theorems · Theorem · commutative algebra

MvPolynomial.universalFactorizationMap_comp_map

∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (n m k : ℕ)
  (hn : n = m + k),
  (MvPolynomial.universalFactorizationMap S n m k hn).comp (MvPolynomial.map (algebraMap R S)) =
    (Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (MvPolynomial.mapAlgHom (Algebra.ofId R S)))
          ((AlgHom.restrictScalars R Algebra.TensorProduct.includeRight).comp
            (MvPolynomial.mapAlgHom (Algebra.ofId R S)))
          ⋯).comp
      (MvPolynomial.universalFactorizationMap R n m k hn).toRingHom

Defined in: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Cited by: 1 results in Mathlib
Foundations: Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites44

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Semiringproof · cited by 13,802
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Polynomialproof · cited by 5,681
Finsuppstatement · cited by 5,255
Algebra.algebraMapstatement and proof · cited by 4,706
mul_oneproof · cited by 3,885
AlgHomstatement · cited by 3,236
one_mulproof · cited by 2,841
TensorProductstatement and proof · cited by 2,545

Cited by1

Results whose statement or proof uses this declaration.

MvPolynomial.finite_universalFactorizationMapproof · cited by 0