Module

Exists_D_ne_zero.lean

Nyll.AlgebraicCurves.Geometry.Exists_D_ne_zero

1 declaration indexed from sourceView source ↗

Module documentation

Exists D ne zero

Imports1

Nyll.AlgebraicCurves.FunctionFields.CurveOver

Imported by6

theorem

exists_D_ne_zero

AlgebraicCurve.exists_D_ne_zero

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_D_ne_zero

Lean source · statement

theorem _root_.AlgebraicCurve.exists_D_ne_zero {K F : Type*} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] : ∃ t : F, KaehlerDifferential.D K F t ≠ 0