IsDomain.tensorProduct_of_injective_algHom_laurentSeries
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsDomain_tensorProduct_of_injective_algHom_laurentSeries
attribute [-simp] ModularCurve.coeffEmb_coeff ModularCurve.coeffMap_coeff ModularCurve.coeffMap_id
ModularCurve.coeffMap_single
open scoped TensorProductLean source · statement
theorem _root_.IsDomain.tensorProduct_of_injective_algHom_laurentSeries
(A : Type*) [CommRing A] [IsDomain A]
(K : Type*) [Field K] [Algebra A K] [IsFractionRing A K]
(D : Type*) [CommRing D] [Nontrivial D] [Algebra A D]
(φ : D →ₐ[A] LaurentSeries K) (hφ : Function.Injective φ)
(L : Type*) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] :
IsDomain (L ⊗[A] D)