Commit 2025-04-27 19:30 fed914b4

View on Github →

chore: prepare for the next lean version bump (#24417) Mostly lemmas that were renamed in core and syntax changes related to dot notation that should not have worked before.

Estimated changes

modified theorem MonoidHom.comap_mker
modified theorem MonoidHom.map_mrange
modified theorem MonoidHom.restrict_mker
modified theorem LinearMap.comp_ker_subtype
modified theorem Int.natAbs_surjective
added theorem Int.coe_lcm_dvd
added theorem Int.dvd_coe_gcd
deleted theorem Int.dvd_gcd
deleted theorem Int.lcm_dvd
modified theorem Int.sqrt_natCast
modified theorem LinearMap.range_mkQ_comp
modified theorem Ideal.map_toCotangent_ker
modified theorem RingHom.comap_ker