Module

Place_ord_add_eq_of_lt.lean

Nyll.AlgebraicCurves.Places.Place_ord_add_eq_of_lt

2 declarations indexed from sourceView source ↗

Module documentation

Place ord add eq of lt

The order of a sum equals the smaller order when the two nonzero summands have unequal orders.

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by13

theorem

ord_add_eq_of_lt

L33 ↗

AlgebraicCurves.Places.Proofs.Place_ord_add_eq_of_lt.AlgebraicCurve.FF2S.ord_add_eq_of_lt

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_add_eq_of_lt
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_add_eq_of_lt (v : Place K F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0)
    (h : v.ord f < v.ord g) : v.ord (f + g) = v.ord f

theorem

ord_add_eq_of_lt

L46 ↗

AlgebraicCurve.Place.ord_add_eq_of_lt

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_add_eq_of_lt

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_add_eq_of_lt {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : AlgebraicCurve.Place K F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (h :
  v.ord f < v.ord g) :
    v.ord (f + g) = v.ord f

Module documentation

Place ord add eq of lt

Declarations

ord_add_eq_of_lt

ord_add_eq_of_lt