theorem TensorSplitting.span_prod_eq_biInf {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (g : ι → R) (hc : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (g i) (g j)) : Ideal.span {∏ i ∈ s, g i} = ⨅ i ∈ s, Ideal.span {g i}

theorem TensorSplitting.span_prod_eq_iInf {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : ι → R) (hc : Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) : Ideal.span {∏ i : ι, g i} = ⨅ (i : ι), Ideal.span {g i}

theorem TensorSplitting.isCoprime_of_irreducible_of_not_associated {K : Type u_1} [Field K] {p q : Polynomial K} (hp : Irreducible p) (hq : Irreducible q) (hne : ¬Associated p q) : IsCoprime p q

theorem TensorSplitting.quotientInfRingEquivPiQuotient_algebraMap {K' : Type u_1} [Field K'] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (I : ι → Ideal (Polynomial K')) (hc : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) (k : K') : (Ideal.quotientInfRingEquivPiQuotient I hc) ((algebraMap K' (Polynomial K' ⧸ ⨅ (i : ι), I i)) k) = (algebraMap K' ((i : ι) → Polynomial K' ⧸ I i)) k

noncomputable def TensorSplitting.quotientInfAlgEquivPiQuotient {K' : Type u_1} [Field K'] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (I : ι → Ideal (Polynomial K')) (hc : Pairwise fun (i j : ι) => IsCoprime (I i) (I j)) : (Polynomial K' ⧸ ⨅ (i : ι), I i) ≃ₐ[K'] (i : ι) → Polynomial K' ⧸ I i

noncomputable def TensorSplitting.adjoinRootProdAlgEquiv {K' : Type u_1} [Field K'] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : ι → Polynomial K') (hc : Pairwise fun (i j : ι) => IsCoprime (g i) (g j)) : AdjoinRoot (∏ i : ι, g i) ≃ₐ[K'] (i : ι) → AdjoinRoot (g i)

noncomputable def TensorSplitting.adjoinRootProdAlgEquiv_of_irreducible {K' : Type u_1} [Field K'] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : ι → Polynomial K') (hirr : ∀ (i : ι), Irreducible (g i)) (hne : Pairwise fun (i j : ι) => ¬Associated (g i) (g j)) : AdjoinRoot (∏ i : ι, g i) ≃ₐ[K'] (i : ι) → AdjoinRoot (g i)

theorem TensorSplitting.polyEquivTensor'_symm_comp_includeRight {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Algebra K K'] : (↑(polyEquivTensor' K K').symm).comp ↑Algebra.TensorProduct.includeRight = Polynomial.mapRingHom (algebraMap K K')

noncomputable def TensorSplitting.adjoinRoot_tensorProduct_algEquiv {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Algebra K K'] (f : Polynomial K) : TensorProduct K (AdjoinRoot f) K' ≃ₐ[K'] AdjoinRoot (Polynomial.map (algebraMap K K') f)

noncomputable def TensorSplitting.adjoinRoot_tensor_algEquiv_prod {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Algebra K K'] {ι : Type u_3} [DecidableEq ι] [Fintype ι] (f : Polynomial K) (_hf_irr : Irreducible f) (_hf_sep : f.Separable) (g : ι → Polynomial K') (hirr : ∀ (i : ι), Irreducible (g i)) (hne : Pairwise fun (i j : ι) => ¬Associated (g i) (g j)) (hprod : Associated (Polynomial.map (algebraMap K K') f) (∏ i : ι, g i)) : TensorProduct K (AdjoinRoot f) K' ≃ₐ[K'] (i : ι) → AdjoinRoot (g i)