AlgebraicCurve.isIntegral_adjoin_of_isScalarTower
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsIntegral_adjoin_of_isScalarTowerLean source · statement
theorem _root_.AlgebraicCurve.isIntegral_adjoin_of_isScalarTower {K L F : Type*} [CommRing K]
[CommRing L] [CommRing F] [Algebra K L] [Algebra K F] [Algebra L F] [IsScalarTower K L F] {j x :
F} (hx : IsIntegral (Algebra.adjoin K {j}) x) : IsIntegral (Algebra.adjoin L {j}) x