Commit 2023-12-08 10:23 d14658b4

View on Github →

chore: Replace (· op ·) a by (a op ·) (#8843) I used the regex \(\(· (.) ·\) (.)\), replacing with ($2 $1 ·).

Estimated changes

modified theorem Equiv.coe_constVAdd
modified theorem Equiv.coe_constVSub
modified theorem Algebra.lsmul_coe
modified theorem Finset.le_sum_card
modified theorem Finset.le_sum_card_inter
modified theorem Finset.sum_card
modified theorem Finset.sum_card_inter
modified theorem Finset.sum_card_inter_le
modified theorem Finset.sum_card_le
modified theorem Multiset.gcd_map_mul
modified theorem mul_left_surjective
modified theorem one_mul_eq_id
modified theorem mul_right_injective
modified theorem Equiv.coe_mulLeft
modified theorem zero_mul_eq_const
modified theorem mul_right_injective₀
modified theorem mulLeft_bijective₀
modified theorem zpow_injective
modified theorem zpow_strictAnti
modified theorem zpow_strictMono
modified theorem antitone_mul_left
modified theorem strictAnti_mul_left
modified theorem preimage_mul_ball
modified theorem preimage_mul_sphere
modified theorem lipschitzWith_smul
modified theorem MulSalemSpencer.mul_left
modified theorem Functor.Comp.map_mk
modified theorem Functor.map_id
modified theorem Finset.filter_le_eq_Ici
modified theorem Finset.filter_lt_eq_Ioi
modified theorem Finset.image_add_left_Icc
modified theorem Finset.image_add_left_Ico
modified theorem Finset.image_add_left_Ioc
modified theorem Finset.image_add_left_Ioo
modified theorem Finset.singleton_div
modified theorem Finset.singleton_mul
modified theorem Finset.singleton_vsub
modified theorem Finset.smul_finset_def
modified def Finsupp.comapSMul
modified theorem Finsupp.comapSMul_def
modified theorem List.Ico.map_add
modified theorem Multiset.map_add_left_Icc
modified theorem Multiset.map_add_left_Ico
modified theorem Multiset.map_add_left_Ioc
modified theorem Multiset.map_add_left_Ioo
modified theorem Set.iUnion_div_left_image
modified theorem Set.iUnion_mul_left_image
modified theorem Set.image_mul_left'
modified theorem Set.image_mul_left
modified theorem Set.preimage_mul_left_one'
modified theorem Set.preimage_mul_left_one
modified theorem Set.singleton_mul
modified theorem Set.image_const_mul_uIcc
modified theorem Set.image_mul_const_uIcc
modified theorem Set.preimage_const_mul_Ici
modified theorem Set.preimage_const_mul_Iic
modified theorem Set.preimage_const_mul_Iio
modified theorem Set.preimage_const_mul_Ioi
modified theorem Set.iUnion_vsub_left_image
modified theorem Set.singleton_vsub
modified theorem Set.iUnion_image_inf_left
modified theorem Set.image_subset_infs_right
modified theorem Flow.isInvariant_omegaLimit
modified theorem Flow.omegaLimit_omegaLimit
modified theorem MulAction.mapsTo_smul_orbit
modified theorem List.smul_prod
modified theorem List.smul_sum
modified theorem Multiset.smul_prod
modified theorem Multiset.smul_sum
modified theorem comp_smul_left
modified theorem one_smul_eq_id
modified theorem Option.smul_def
modified theorem Sigma.smul_def
modified theorem Sum.smul_def
modified theorem Equiv.swap_mul_involutive
modified theorem AffineEquiv.coe_constVSub
modified theorem MeasurableEquiv.coe_mulLeft
modified theorem MeasurableEquiv.coe_smul₀
modified theorem measurableEmbedding_mulLeft
modified theorem monotone_le
modified theorem monotone_lt
modified theorem Filter.mem_smul_filter
modified theorem Filter.pure_div
modified theorem Filter.pure_mul
modified theorem Filter.pure_smul
modified theorem Filter.pure_vsub
modified theorem bihimp_right_injective
modified theorem bihimp_right_involutive
modified theorem bihimp_right_surjective
modified theorem symmDiff_right_injective
modified theorem symmDiff_right_involutive
modified theorem symmDiff_right_surjective
modified theorem Ordinal.add_isNormal
modified theorem Ordinal.mul_isNormal
modified theorem Homeomorph.coe_mulLeft
modified theorem Homeomorph.coe_mulRight
modified theorem continuous_div_left'
modified theorem continuous_div_right'
modified theorem isClosedMap_div_left
modified theorem isClosedMap_div_right
modified theorem isClosedMap_mul_left
modified theorem isClosedMap_mul_right
modified theorem isOpenMap_div_left
modified theorem isOpenMap_div_right
modified theorem isOpenMap_mul_left
modified theorem isOpenMap_mul_right
modified theorem map_mul_left_nhds
modified theorem map_mul_left_nhds_one
modified theorem map_mul_right_nhds
modified theorem map_mul_right_nhds_one
modified theorem nhds_translation_mul_inv
modified theorem Metric.preimage_smul_ball