NYLL
Module

Place_min_ord_le_ord_add.lean

Nyll.AlgebraicCurves.Places.Place_min_ord_le_ord_add
2 declarations indexed from sourceView source ↗

Module documentation

Place min ord le ord add

The order of a nonzero sum is bounded below by the minimum of the summands’ orders.

Imports1
Imported by15

Declarations

theorem

le_ord_add

L33 ↗
AlgebraicCurves.Places.Proofs.Place_min_ord_le_ord_add.AlgebraicCurve.FF2S.le_ord_add
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_min_ord_le_ord_add
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 le_ord_add (v : Place K F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (hfg : f + g ≠ 0) :
    min (v.ord f) (v.ord g) ≤ v.ord (f + g)
theorem

min_ord_le_ord_add

L49 ↗
AlgebraicCurve.Place.min_ord_le_ord_add
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_min_ord_le_ord_add
Lean source · statement
theorem _root_.AlgebraicCurve.Place.min_ord_le_ord_add {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : AlgebraicCurve.Place K F) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (hfg :
  f + g ≠ 0) :
    min (v.ord f) (v.ord g) ≤ v.ord (f + g)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.