theorem
L25 ↗finrankAlong_comp
AlgebraicCurve.finrankAlong_comp
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FinrankAlong_comp
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.finrankAlong_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'') :
AlgebraicCurve.finrankAlong K (χ.comp φ) = AlgebraicCurve.finrankAlong K φ *
AlgebraicCurve.finrankAlong K χ