Commit 2025-09-02 01:48 13e87026

View on Github →

chore: remove >6 month old deprecations (incomplete) (#29197)

Estimated changes

deleted theorem bddBelow_image_norm
deleted theorem image_norm_nonempty
deleted theorem isGLB_quotient_norm
deleted theorem norm_mk_eq_zero
deleted theorem norm_mk_lt'
deleted theorem norm_mk_lt
deleted theorem norm_mk_nonneg
deleted theorem norm_mk_zero
deleted theorem quotient_nhds_basis
deleted theorem quotient_norm_eq_zero_iff
deleted theorem quotient_norm_mk_le'
deleted theorem quotient_norm_mk_le
deleted theorem quotient_norm_neg
deleted theorem quotient_norm_nonneg
deleted theorem quotient_norm_sub_rev