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