Commit 2025-03-17 01:20 5449dc90
View on Github →feat: add some elementary number theory lemmas (#22989)
This PR adds a few elementary lemmas of a number theoretic flavor. It also improves the sectioning in Mathlib/RingTheory/Fintype.lean.
See here on Zulip.
I'm labeling this t-number-theory although the modified files are under Data and RingTheory.