Commit 2026-03-02 10:51 ed1c732d

View on Github →

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

Estimated changes

added def WithVal.algEquiv
added theorem WithVal.algEquiv_apply
modified theorem WithVal.apply_equiv
modified theorem WithVal.apply_symm_equiv
added def WithVal.congr
added theorem WithVal.congr_apply
added theorem WithVal.congr_refl
added theorem WithVal.congr_symm
added theorem WithVal.congr_trans
modified def WithVal.equiv
modified theorem WithVal.le_def
modified theorem WithVal.lt_def
added def WithVal.map
added theorem WithVal.map_apply
added theorem WithVal.map_comp
added theorem WithVal.map_id
added theorem WithVal.ofVal_add
added theorem WithVal.ofVal_div
added theorem WithVal.ofVal_eq_zero
added theorem WithVal.ofVal_inv
added theorem WithVal.ofVal_mul
added theorem WithVal.ofVal_neg
added theorem WithVal.ofVal_one
added theorem WithVal.ofVal_pow
added theorem WithVal.ofVal_smul
added theorem WithVal.ofVal_sub
added theorem WithVal.ofVal_toVal
added theorem WithVal.ofVal_zero
added theorem WithVal.smul_left_def
added theorem WithVal.smul_right_def
added theorem WithVal.toVal_add
added theorem WithVal.toVal_div
added theorem WithVal.toVal_eq_zero
added theorem WithVal.toVal_inv
added theorem WithVal.toVal_mul
added theorem WithVal.toVal_neg
added theorem WithVal.toVal_ofVal
added theorem WithVal.toVal_one
added theorem WithVal.toVal_pow
added theorem WithVal.toVal_smul
added theorem WithVal.toVal_sub
added theorem WithVal.toVal_zero
added structure WithVal
deleted def WithVal