Theorem Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective

Modification history

2026-10-16 07:34
Mathlib/RingTheory/Valuation/Discrete/Basic.lean
chore: remove declarations deprecated between 2026-04-01 and 2026-04-15 (#44903) …
Deleted Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjectiveView on Github →
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_neg_exp_one_of_surjectiveView on Github →
2026-03-06 13:45
Mathlib/RingTheory/Valuation/Discrete/RankOne.lean
chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain (#26872) …
Added Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjectiveView on Github →