Commit 2023-11-19 01:23 c8d9ed0f
View on Github →feat(Data/Nat): add Nat.div_pow (#8327)
Adds the missing lemma Nat.div_pow, which seemed to be missing (at least, exact?% couldn't find it with all of Mathlib imported). Also moves div_mul_div_comm higher in the hierarchy (and golf) because it doesn't need the ordered semiring instance, cf the docstring of Data/Nat/Order/Basic.