Commit 2025-02-11 11:58 7f847703

View on Github →

chore: deal with an erw in NumberTheory.Multiplicity (#21700)

Estimated changes

added theorem Int.natCast_dvd_ofNat
added theorem Int.ofNat_dvd_natCast