Commit 2026-04-01 15:51 865d1508
View on Github →feat(Valuation/Discrete/RankOne): generalize results to Ring (#37497)
This PR generalize the RankOne file to use Ring instead of CommRing and Field.
The lemma generator_eq_neg_exp_one_of_surjective has been renamed to generator_eq_exp_neg_one_of_surjective.
This same lemma is also generalized in the form of generator_eq_exp_neg_one_of_mem_range.