Theorems · Theorem · commutative algebra

Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd

∀ {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) (p : Polynomial.MonicDegreeEq R n) {T : Type u_4} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (f : Polynomial.UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) (g : S →ₐ[R] T),
  (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv T m k hn p) (g.comp f))).2 =
    (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv S m k hn p) f)).2.map ↑g

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

1 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebra