Documentation

Atlas.NumberTheoryI.code.Chapter1.LocalRings

source
@[reducible, inline]
abbrev LocalRings.IsLocalRingDef (A : Type u_1) [CommRing A] :
Prop
Instances For
    source
    @[reducible, inline]
    abbrev LocalRings.residueFieldOfLocal (A : Type u_1) [CommRing A] [IsLocalRing A] :
    Type u_1
    Instances For