Theorem Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range

Modification history

2026-06-08 09:51
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
feat(DedekindDomain/AdicValuation): `intValuation` on uniformizers is `exp (-1)` (#37501) …
Modified Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_rangeView on Github →
2026-04-01 15:51
Mathlib/RingTheory/Valuation/Discrete/RankOne.lean
feat(Valuation/Discrete/RankOne): generalize results to Ring (#37497) …
Added Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_rangeView on Github →