Commit 2025-04-09 10:22 d7d140ed

View on Github →

chore: use mixin ordered algebraic typeclasses (part 2) (#20595)

Estimated changes

modified theorem AddConstMapClass.map_fract
modified theorem spectrum_nonneg_of_nonneg
modified theorem Function.Periodic.image_Icc
modified theorem Function.Periodic.image_Ioc
modified theorem Int.fract_periodic
modified theorem Odd.geom_sum_pos
modified theorem geom_sum_Ico_le_of_lt_one
modified theorem geom_sum_lt
modified theorem geom_sum_ne_zero
modified theorem geom_sum_neg_iff
modified theorem geom_sum_of_lt_one
modified theorem geom_sum_of_one_lt
modified theorem geom_sum_pos'
modified theorem geom_sum_pos
modified theorem geom_sum_pos_and_lt_one
modified theorem geom_sum_pos_iff
modified theorem geom₂_sum_of_gt
modified theorem geom₂_sum_of_lt
modified theorem MulEquiv.strictMono_symm
modified theorem exists_lt_pow
modified theorem exists_nat_ge
modified theorem AbsoluteValue.sum_le
modified theorem Finset.abs_prod
modified theorem IsAbsoluteValue.abv_sum
modified theorem IsAbsoluteValue.map_prod
modified def CauSeq
modified def IsCauSeq
modified def FloorRing.ofCeil
modified def FloorRing.ofFloor
modified theorem Int.ceil_nonneg
modified theorem Int.floor_nonpos
modified theorem Nat.le_floor
modified theorem subsingleton_floorRing
modified theorem Nat.ceil_intCast
modified theorem Nat.floor_add_natCast
modified theorem Nat.floor_congr
modified theorem Nat.map_floor
modified theorem subsingleton_floorSemiring
modified theorem Nonneg.nat_ceil_coe
modified theorem Nonneg.nat_floor_coe
modified theorem one_le_pow_mul_abs_eval_div
modified theorem CHSH_inequality_of_comm
modified theorem tsirelson_inequality
modified theorem Set.OrdConnected.convex
modified theorem convex_iff_ordConnected
modified def affineSegment
modified theorem ConvexCone.coe_mk
modified theorem ConvexCone.mem_mk
modified structure ConvexCone
modified structure ProperCone
modified theorem IsExposed.sInter
modified theorem IsExtreme.convex_diff
modified theorem ConcaveOn.add_const
modified theorem ConvexOn.add_const
modified theorem StrictConcaveOn.add_const
modified theorem StrictConvexOn.add_const
modified theorem sameRay_of_mem_segment
modified theorem Set.OrdConnected.starConvex
modified def StarConvex
modified theorem starConvex_iff_ordConnected
modified def StrictConvex
modified theorem Tendsto.den
modified theorem Tendsto.num
modified theorem tendsto_nat_ceil_atTop
modified theorem tendsto_nat_floor_atTop
modified theorem tendsto_nat_floor_mul_atTop
modified theorem threeAPFree_frontier
modified theorem Finpartition.coe_energy
modified def doublyStochastic
modified theorem Rat.isInt_intCeil
modified theorem Rat.isInt_intFloor
modified theorem Rat.isNat_intCeil
modified theorem Rat.isNat_intFloor
modified theorem dotProduct_self_eq_zero
modified theorem QuadraticMap.PosDef.smul
modified theorem QuadraticMap.nonneg_pi_iff
modified theorem QuadraticMap.posDef_pi_iff
modified def SameRay
modified theorem Measurable.fract
modified theorem Measurable.nat_floor
modified theorem MeasurableSet.image_fract
modified theorem Nat.measurable_floor
modified theorem measurable_fract
modified theorem MeasureTheory.setToFun_mono
modified theorem ClassGroup.norm_lt
modified theorem Int.comap_cast_atBot
modified theorem Int.comap_cast_atTop
modified theorem Nat.comap_cast_atTop
modified theorem Rat.comap_cast_atBot
modified theorem Rat.comap_cast_atTop
modified theorem tendsto_intCast_atBot_iff
modified theorem tendsto_intCast_atTop_atTop
modified theorem tendsto_intCast_atTop_iff
modified theorem tendsto_natCast_atTop_atTop
modified theorem tendsto_natCast_atTop_iff
modified theorem tendsto_ratCast_atBot_iff
modified theorem tendsto_ratCast_atTop_iff
modified theorem Polynomial.cyclotomic_pos'
modified theorem Polynomial.cyclotomic_pos
modified theorem Linarith.add_neg
modified theorem Linarith.add_nonpos
modified theorem Linarith.eq_of_eq_of_eq
modified theorem Linarith.le_of_eq_of_le
modified theorem Linarith.le_of_le_of_eq
modified theorem Linarith.lt_of_eq_of_lt
modified theorem Linarith.lt_of_lt_of_eq
modified theorem Linarith.mul_eq
modified theorem Linarith.mul_neg
modified theorem Linarith.mul_nonpos
modified theorem Linarith.natCast_nonneg
modified theorem Linarith.sub_neg_of_lt
modified theorem Linarith.sub_nonpos_of_le
modified theorem Linarith.zero_lt_one
modified theorem affineHomeomorph_image_Icc
modified theorem affineHomeomorph_image_Ico
modified theorem affineHomeomorph_image_Ioc
modified theorem affineHomeomorph_image_Ioo
modified theorem Finite.of_summable_const
modified theorem hasProd_of_isLUB
modified theorem hasProd_of_isLUB_of_one_le
modified theorem multipliable_mabs_iff
modified theorem tprod_subtype_le
modified theorem locallyConvexSpace_inf
modified theorem Rat.denseRange_cast
modified theorem IsTopologicalRing.of_norm
modified theorem continuousOn_ceil
modified def AbsoluteValue.comp
modified def ValuedCSP.binaryTerm
modified def ValuedCSP.unaryTerm