Commit 2025-04-04 17:16 7508a9e2

View on Github →

chore: use mixin ordered algebraic typeclasses (part 1) (#20594)

Estimated changes

modified theorem finprod_cond_nonneg
modified theorem finprod_nonneg
modified theorem one_le_finprod'
modified theorem one_lt_finprod'
modified theorem single_le_finprod
modified theorem Finset.prod_Ico_add'
modified theorem Finset.prod_Ico_add
modified theorem AbsoluteValue.listSum_le
modified structure AbsoluteValue
modified theorem Finset.abs_sum_le_sum_abs
modified theorem Finset.abs_sum_of_nonneg'
modified theorem Finset.abs_sum_of_nonneg
modified theorem Finset.max_prod_le
modified theorem Finset.prod_min_le
modified theorem List.one_lt_prod_of_one_lt
modified theorem List.prod_eq_one_iff
modified theorem List.single_le_prod
modified theorem Multiset.abs_sum_le_sum_abs
modified theorem Multiset.max_prod_le
modified theorem Multiset.prod_eq_one_iff
modified theorem Multiset.prod_min_le
modified theorem inv_mul_le_one
modified theorem mul_inv_le_one
modified theorem ceilDiv_one
modified theorem floorDiv_one
modified theorem abs_sub_map_le_div
modified theorem map_pos_of_ne_one
modified theorem OrderMonoidHom.coe_mul
modified theorem OrderMonoidHom.comp_mul
modified theorem OrderMonoidHom.mul_apply
modified theorem OrderMonoidHom.mul_comp
modified theorem Set.mem_Icc_iff_abs_le
modified theorem OrderedSMul.mk''
modified theorem exists_abs_lt
modified theorem Units.mem_posSubgroup
modified def Units.posSubgroup
modified theorem IsSumSq.nonneg
modified theorem Tropical.mul_eq_zero_iff
modified theorem Set.IsPWO.mul
modified theorem Nat.cast_max
modified theorem Nat.cast_min
modified theorem Nat.cast_nonneg
modified theorem Nat.cast_pos
modified theorem Nat.cast_tsub
modified theorem Nat.ofNat_nonneg
modified theorem Nat.ofNat_pos
modified theorem sign_intCast
modified theorem AffineMap.image_uIcc
modified theorem Filter.comap_mabs_atTop
modified theorem Filter.inv_atTop
modified def orderIsoIooNegOneOne
modified theorem IsCoprime.sq_add_sq_ne_zero
modified theorem HahnModule.one_smul'
modified theorem HahnSeries.order_mul
modified theorem HahnSeries.order_pow
modified theorem orderTopology_of_nhds_mabs
modified theorem UniformSpace.hasBasis_ofFun
modified def UniformSpace.ofFun