Commit 2024-01-09 17:40 47a02614

View on Github →

chore: Move x ⊔ y = (x + y + |y - x|) / 2 (#9466) Part of #9411

Estimated changes

Modified Mathlib/Algebra/Order/Group/PosPart.lean

deleted theorem inf_eq_half_smul_add_sub_abs_sub'

deleted theorem inf_eq_half_smul_add_sub_abs_sub

deleted theorem sup_eq_half_smul_add_add_abs_sub'

deleted theorem sup_eq_half_smul_add_add_abs_sub

Modified Mathlib/Algebra/Order/Module/OrderedSMul.lean

added theorem inf_eq_half_smul_add_sub_abs_sub'

added theorem inf_eq_half_smul_add_sub_abs_sub

added theorem sup_eq_half_smul_add_add_abs_sub'

added theorem sup_eq_half_smul_add_add_abs_sub