Commit 2026-03-02 16:30 19d4af96

View on Github →

refactor: use 1-field structure to define the WithAbs type synonym (#34230) Following the Zulip threads here and here and using WithLp as a template, we refactor the WithAbs type synonym as a 1-field structure. The main benefit being that it prevents defeq abuse.

Estimated changes

modified theorem WithAbs.isometry_of_comp
added theorem WithAbs.ofAbs_div
added theorem WithAbs.ofAbs_inv
added theorem WithAbs.toAbs_div
added theorem WithAbs.toAbs_inv
modified def WithAbs.algEquiv
added theorem WithAbs.algEquiv_apply
added def WithAbs.congr
added theorem WithAbs.congr_apply
added theorem WithAbs.congr_refl
added theorem WithAbs.congr_symm
added theorem WithAbs.congr_trans
modified def WithAbs.equiv
added def WithAbs.map
added theorem WithAbs.map_apply
added theorem WithAbs.map_comp
added theorem WithAbs.map_id
deleted theorem WithAbs.norm_eq_abv
added theorem WithAbs.norm_toAbs_eq
added theorem WithAbs.ofAbs_add
added theorem WithAbs.ofAbs_eq_zero
added theorem WithAbs.ofAbs_mul
added theorem WithAbs.ofAbs_neg
added theorem WithAbs.ofAbs_one
added theorem WithAbs.ofAbs_pow
added theorem WithAbs.ofAbs_sub
added theorem WithAbs.ofAbs_toAbs
added theorem WithAbs.ofAbs_zero
added theorem WithAbs.smul_left_def
added theorem WithAbs.smul_right_def
added theorem WithAbs.toAbs_add
added theorem WithAbs.toAbs_eq_zero
added theorem WithAbs.toAbs_mul
added theorem WithAbs.toAbs_neg
added theorem WithAbs.toAbs_ofAbs
added theorem WithAbs.toAbs_one
added theorem WithAbs.toAbs_pow
added theorem WithAbs.toAbs_sub
added theorem WithAbs.toAbs_zero
added structure WithAbs
deleted def WithAbs