Commit 2025-07-05 02:43 ab65d46b

doc(Data/Nat/Modeq): fix a couple of doc comment issues (#26750)

• nat is now spelled Nat.
• Defining a ≡ b [MOD n] to mean "a - b is a multiple of n" does not make sense for the Lean naturals, which have saturating subtraction. Consider (a,b,n) = (1, 2, 3). (This comment was added in https://github.com/leanprover-community/mathlib3/commit/1dddcf69ecd7edfa3c9ebc4faf0723df8ff128ca)