mathlib3
c163ec99 - chore(ring_theory/discrete_valuation_ring): create folder ring_theory/discrete_valuation_ring (#18867)

Commit
2 years ago
chore(ring_theory/discrete_valuation_ring): create folder ring_theory/discrete_valuation_ring (#18867) Moved the file `ring_theory/discrete_valuation_ring.lean` inside the folder and renamed it as `basic.lean`; also, added the file `valuation.tfae` giving equivalent conditions for being a dvr to the folder.
Author
Parents
Loading