Commit 2023-06-06 12:22 c072e185

View on Github →

feat: port RingTheory.Valuation.ValuationRing (#4720)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/ValuationRing.lean

added theorem Function.Surjective.valuationRing

added def ValuationRing.ValueGroup

added theorem ValuationRing.coe_equivInteger_apply

added theorem ValuationRing.cond

added theorem ValuationRing.dvd_total

added theorem ValuationRing.iff_dvd_total

added theorem ValuationRing.iff_ideal_total

added theorem ValuationRing.iff_isInteger_or_isInteger

added theorem ValuationRing.iff_local_bezout_domain

added theorem ValuationRing.isInteger_or_isInteger

added theorem ValuationRing.mem_integer_iff

added theorem ValuationRing.of_integers

added theorem ValuationRing.range_algebraMap_eq

added theorem ValuationRing.unique_irreducible

added def ValuationRing.valuation