adamtopaz

/-
Copyright (c) 2022 Sam van Gool and Jake Levinson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sam van Gool, Jake Levinson
-/

import topology.sheaves.presheaf
import topology.sheaves.stalks

/-!

adamtopaz

URxvt.font: xft:terminus:style=Regular:size=12
URxvt.boldFont: xft:terminus:style=Bold:size=12
URxvt.italicFont: xft:terminus:style=Italic:size=12
URxvt.boldItalicFont: xft:terminus:style=Bold Italic:size=12
URxvt.letterSpace: 0
URxvt.lineSpace: 0
URxvt.geometry: 92x24
URxvt.internalBorder: 5 
URxvt.cursorBlink: true
URxvt.cursorUnderline: false

adamtopaz

import ring_theory.algebra
import linear_algebra

variables (R : Type*) [comm_ring R]
variables (M : Type*) [add_comm_group M] [module R M]

inductive pre
| of : M → pre
| zero : pre
| one : pre

adamtopaz

import ring_theory.principal_ideal_domain

class DVR (A : Type*) extends principal_ideal_domain A  :=
(val_cond : ∀ x y : A, ∃ z : A, x * z = y ∨ y * z = x) -- i.e. a valuation ring
(nonfield : ∃ u : A, ∀ v : A, u * v ≠ 1) -- or a better formulation

open DVR 

instance local_ring_of_dvr (A : Type*) [DVR A] : local_ring A := 
begin

adamtopaz

Keybase proof

I hereby claim:

• I am adamtopaz on github.
• I am atopaz (https://keybase.io/atopaz) on keybase.
• I have a public key whose fingerprint is 7C8C FEFE 6DA2 3A5D FE6F 7154 08B2 EFF4 E8D0 2A3A

To claim this, I am signing this object: