AlgebraicCurve.finiteAlong_of_isIntegral
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FiniteAlong_of_isIntegral
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.finiteAlong_of_isIntegral
{K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
[Algebra.EssFiniteType K F']
(φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) :
FiniteAlong K φ