Commit 2024-07-30 01:09 ee1fbad9

View on Github →

chore: backports for leanprover/lean4#4814 (part 4) (#15255) See https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

modified theorem AddMonoidHom.apply_int
modified def zmultiplesAddHom
modified theorem zmultiplesAddHom_apply
modified theorem zmultiplesAddHom_symm_apply
modified def zmultiplesHom
modified theorem zmultiplesHom_apply
modified theorem zmultiplesHom_symm_apply
modified theorem List.mapIdxM_eq_mmap_enum
modified theorem List.sizeOf_dedupKeys
modified theorem List.sizeOf_kerase
modified theorem AddMonoidHom.apply_nat
modified def multiplesAddHom
modified theorem multiplesAddHom_apply
modified theorem multiplesAddHom_symm_apply
modified def multiplesHom
modified theorem multiplesHom_apply
modified theorem multiplesHom_symm_apply
modified theorem AntitoneOn.map_bddAbove
modified theorem AntitoneOn.map_bddBelow
modified theorem AntitoneOn.map_isGreatest
modified theorem AntitoneOn.map_isLeast
modified theorem MonotoneOn.map_bddAbove
modified theorem MonotoneOn.map_bddBelow
modified theorem MonotoneOn.map_isGreatest
modified theorem MonotoneOn.map_isLeast
modified theorem sSup_eq_bot'