Module

Place_ord_natCast.lean

Nyll.AlgebraicCurves.Places.Place_ord_natCast

2 declarations indexed from sourceView source ↗

Module documentation

Place ord nat Cast

Imports2

Imported by4

theorem

ord_natCast

L31 ↗

AlgebraicCurves.Places.Proofs.Place_ord_natCast.AlgebraicCurve.FF2S.ord_natCast

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_natCast
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2S
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_natCast (v : Place K F) (n : ℕ) : v.ord (n : F) = 0

theorem

ord_natCast

L37 ↗

AlgebraicCurve.Place.ord_natCast

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_natCast

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_natCast {K F : Type*} [Field K] [Field F] [Algebra K F] (v
  : AlgebraicCurve.Place K F) (n : ℕ) :
    v.ord (n : F) = 0

Module documentation

Place ord nat Cast

Declarations

ord_natCast

ord_natCast