Module

PlainIntegerBase.lean

Nyll.SchemeTheory.FunctionFields.PlainIntegerBase

1 declaration indexed from sourceView source ↗

Module documentation

Imports3

Imported by4

def

AlgebraicGeometry.specZGenericResidueFieldEquivQ

Documentation

The generic residue field of the ordinary spectrum of the integers is canonically isomorphic to the rationals.

Source context 3 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry

Lean source · statement

def specZGenericResidueFieldEquivQ :
    (Spec (CommRingCat.of ℤ)).residueField
      (genericPoint (Spec (CommRingCat.of ℤ))) ≃+* ℚ