Module

FinrankAlong_id.lean

Nyll.AlgebraicCurves.FunctionFields.FinrankAlong_id

1 declaration indexed from sourceView source ↗

Module documentation

Imports1

Imported by2

theorem

AlgebraicCurve.finrankAlong_id

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FinrankAlong_id

Lean source · statement

theorem _root_.AlgebraicCurve.finrankAlong_id {K F : Type*} [Field K] [Field F] [Algebra K F] :
    AlgebraicCurve.finrankAlong K (AlgHom.id K F) = 1