AlgebraicCurve.finrankAlong_eq_relfinrank_fieldRange
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FinrankAlong_eq_relfinrank_fieldRangeLean source · statement
theorem _root_.AlgebraicCurve.finrankAlong_eq_relfinrank_fieldRange {K E : Type*} [Field K] [Field
E] [Algebra K E]
(A B : IntermediateField K E) (phi : A →ₐ[K] B) :
AlgebraicCurve.finrankAlong K phi =
IntermediateField.relfinrank ((B.val.comp phi).fieldRange) B