Module

Place_exists_not_mem_and_forall_ne_mem.lean

Nyll.AlgebraicCurves.Places.Place_exists_not_mem_and_forall_ne_mem

2 declarations indexed from sourceView source ↗

Module documentation

Place exists not mem and forall ne mem

Distinct places separate valuation-subring membership: a function can be excluded from one place while belonging to each place in a finite collection of others.

Imports6

Imported by2

theorem

adicValuation_le_one_iff_mem

L69 ↗

AlgebraicCurve.Place.adicValuation_le_one_iff_mem

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_not_mem_and_forall_ne_mem
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-instance] AlgebraicCurve.Place.instIsPrimeCenter
attribute [-instance] AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance] AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
attribute [-instance]
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.differentialCoeff_zero
  AlgebraicCurve.Place.differentialCoeff_dCoord AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.injEq AlgebraicCurve.TranscendenceTower.mk.injEq
  AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
  AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem _root_.AlgebraicCurve.Place.adicValuation_le_one_iff_mem (v : Place K F) {f : F} :
    v.adicValuation f ≤ 1 ↔ f ∈ v.toValuationSubring

theorem

exists_not_mem_and_forall_ne_mem

L103 ↗

AlgebraicCurve.Place.exists_not_mem_and_forall_ne_mem

Source context 14 commands