Module

Place_ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg.lean

Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg

2 declarations indexed from sourceView source ↗

Module documentation

Place ord nonneg of is Integral adjoin of ord nonneg

Imports4

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg_impl

L34 ↗

AlgebraicCurves.Places.Proofs.Place_ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg.AlgebraicCurve.Place.ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg_impl

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve

Lean source · statement

theorem ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg_impl {K F : Type*} [Field K] [Field
  F] [Algebra K F]
    (v : Place K F) {j u : F} (hu : IsIntegral (Algebra.adjoin K {j}) u) (hj : 0 ≤ v.ord j) :
    0 ≤ v.ord u

theorem

ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg

L46 ↗

AlgebraicCurve.Place.ord_nonneg_of_isIntegral_adjoin_of_ord_nonneg

Source context 2 commands