Commit 2024-04-23 11:47 c1609892

View on Github →

feat(RingTheory/Valuation/RankOne): add rank one valuations (#12156) Add the definition of rank one valuation, as well as some basic lemmas.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/RankOne.lean

added theorem Valuation.RankOne.hom_eq_zero_iff

added theorem Valuation.RankOne.nontrivial

added theorem Valuation.RankOne.strictMono

added def Valuation.RankOne.unit

added theorem Valuation.RankOne.unit_ne_one

added theorem Valuation.RankOne.zero_of_hom_zero