Commit 2024-11-29 23:24 c6be01e3

View on Github →

chore: split out map_dvd (#19565)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Divisibility/Basic.lean

deleted theorem MonoidHom.map_dvd

deleted theorem MulHom.map_dvd

deleted theorem map_dvd

Created Mathlib/Algebra/Divisibility/Hom.lean

added theorem MonoidHom.map_dvd

added theorem MulHom.map_dvd

added theorem map_dvd

Modified Mathlib/Algebra/Prime/Lemmas.lean

Modified Mathlib/Algebra/Ring/Divisibility/Basic.lean

Modified Mathlib/Algebra/Ring/Hom/Basic.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean