Commit 2026-10-17 12:17 e96b7335
View on Github →feat(Data/Nat/ModEq): add congruence mod lcm lemma (#44839)
The new lemma is just a version of modEq_and_modEq_iff_modEq_mul without the coprimality assumption. As a bonus, the proof of modEq_and_modEq_iff_modEq_mul is simplified as well.