Commit 2025-01-25 06:17 25224336

View on Github →

chore(Data/Nat/Cast): don't import MonoidWithZero for results about MonoidHom (#20745) For this, move the results from Data.Nat.Cast.Basic not mentioning Nat.cast (!) to a new file Algebra.Group.Nat.Hom. See https://github.com/leanprover-community/mathlib3/pull/2957 for the copyright attribution.

Estimated changes

added theorem AddMonoidHom.apply_nat
added theorem AddMonoidHom.ext_nat
added theorem MonoidHom.apply_mnat
added theorem MonoidHom.ext_mnat
added theorem ext_nat'
added def multiplesAddHom
added theorem multiplesAddHom_apply
added def multiplesHom
added theorem multiplesHom_apply
added def powersHom
added theorem powersHom_apply
added theorem powersHom_symm_apply
added def powersMulHom
added theorem powersMulHom_apply
deleted theorem AddMonoidHom.apply_nat
deleted theorem AddMonoidHom.ext_nat
deleted theorem MonoidHom.apply_mnat
deleted theorem MonoidHom.ext_mnat
deleted theorem ext_nat'
deleted def multiplesAddHom
deleted theorem multiplesAddHom_apply
deleted def multiplesHom
deleted theorem multiplesHom_apply
deleted theorem multiplesHom_symm_apply
deleted def powersHom
deleted theorem powersHom_apply
deleted theorem powersHom_symm_apply
deleted def powersMulHom
deleted theorem powersMulHom_apply
deleted theorem powersMulHom_symm_apply