def AdjoinRoot.tensorAlgEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S)) (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q) : TensorProduct R T (AdjoinRoot p) ≃ₐ[T] AdjoinRoot q

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AdjoinRoot.tensorAlgEquiv_root {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S)) (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q) : (tensorAlgEquiv p q h) (1 ⊗ₜ[R] root p) = root q

@[simp]

theorem AdjoinRoot.tensorAlgEquiv_of {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (p : Polynomial S) (q : Polynomial (TensorProduct R T S)) (h : Polynomial.map Algebra.TensorProduct.includeRight.toRingHom p = q) {x : S} : (tensorAlgEquiv p q h) (1 ⊗ₜ[R] (of p) x) = (of q) (1 ⊗ₜ[R] x)