Module

Place_eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain.lean

Nyll.AlgebraicCurves.Places.Place_eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain

2 declarations indexed from sourceView source ↗

Module documentation

Place eq of forall coe mem nonunits iff of is Dedekind Domain

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by2

theorem

mem_iff_exists

L30 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain.Ws47.U1.mem_iff_exists

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain
namespace Ws47
namespace U1
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : Subalgebra K F)
  [IsDedekindDomain ↥A] [IsFractionRing ↥A F]

Lean source · statement

theorem mem_iff_exists (v : AlgebraicCurve.Place K F) (hv : ∀ a : ↥A, (a : F) ∈
  v.toValuationSubring) (x : F) :
    x ∈ v.toValuationSubring ↔
      ∃ a s : ↥A, (s : F) ∉ v.toValuationSubring.nonunits ∧ x * (s : F) = (a : F)

theorem

eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain

L129 ↗

AlgebraicCurve.Place.eq_of_forall_coe_mem_nonunits_iff_of_isDedekindDomain

Source context 2 commands