Commit 2023-07-02 14:32 6c1021b5

View on Github →

fix: precedence of ⁺, ⁻ and abs (#5619)

Estimated changes

modified theorem abs_inv
modified theorem abs_by_cases
modified theorem abs_le_max_abs_abs
modified theorem abs_max_le_max_abs_abs
modified theorem abs_min_le_max_abs_abs
modified theorem min_abs_abs_le_abs_max
modified theorem min_abs_abs_le_abs_min
modified theorem abs_max_sub_max_le_max
modified theorem abs_min_sub_min_le_max
modified theorem even_abs
modified theorem Real.ennnorm_eq_ofReal_abs
modified theorem Real.logb_abs
modified theorem Real.log_abs
modified theorem Real.abs_sinh
modified theorem Complex.int_cast_abs
modified theorem Real.cos_abs
modified theorem Real.cosh_abs
modified theorem Int.natAbs_abs
modified theorem EReal.abs_def
modified theorem Hyperreal.infinite_abs_iff
modified theorem MeasureTheory.Lp.coeFn_abs
modified theorem MeasureTheory.Memℒp.abs
modified theorem circleMap_mem_sphere'
modified theorem image_circleMap_Ioc
modified theorem range_circleMap
modified theorem Real.volume_interval
modified theorem Filter.Germ.const_abs
modified theorem ContinuousMap.abs_apply