Commit 2024-05-31 00:19 ac59a83c

View on Github →

chore: fix formatting of many misplaced "by"s (#13204)

Estimated changes

modified theorem gcd_mul_right'
modified theorem div_mul_cancel
modified theorem div_mul_div_cancel'
modified theorem div_mul_eq_div_div_swap
modified theorem eq_iff_eq_of_div_eq_div
modified theorem eq_of_one_div_eq_one_div
modified theorem mul_div_assoc
modified theorem mul_div_cancel_right
modified theorem mul_eq_one_iff_inv_eq
modified theorem mul_mul_mul_comm
modified theorem mul_one_div
modified theorem mul_rotate'
modified theorem mul_rotate
modified theorem inv_eq_of_mul_eq_one_left
modified theorem inv_mul_cancel_left
modified theorem inv_mul_cancel_right
modified theorem mul_inv_cancel_left
modified theorem mul_inv_cancel_right
modified theorem mul_right_inv
modified theorem map_mul_eq_one
modified theorem MulOpposite.semiconjBy_op
modified theorem Subgroup.comap_map_eq_self
modified theorem Subgroup.map_comap_eq_self
modified theorem Subgroup.map_eq_range_iff
modified theorem Subgroup.sup_eq_closure
modified theorem Submonoid.disjoint_def
modified theorem divp_eq_div
modified theorem IsSl2Triple.lie_h_e_smul
modified theorem div_le_div₀
modified theorem toIcoDiv_sub_zsmul'
modified theorem toIcoMod_add_right_eq_add
modified theorem toIcoMod_add_toIocMod_zero
modified theorem toIocDiv_sub_zsmul'
modified theorem toIocMod_add_right_eq_add
modified theorem toIocMod_add_toIcoMod_zero
modified theorem Polynomial.coeff_X_pow_mul
modified theorem Polynomial.eraseLead_coeff
modified theorem Polynomial.eval₂_map
modified theorem conjugate_le_conjugate'
modified theorem conformalAt_iff'
modified theorem ContDiffAt.neg
modified theorem derivWithin_div_const
modified theorem differentiableWithinAt_univ
modified theorem fderiv_mem_iff
modified theorem hasFDerivAt_inv'
modified theorem HasDerivAt.comp_ofReal
modified theorem Convex.affinity
modified theorem convex_iff_ordConnected
modified theorem NormedSpace.exp_unop
modified theorem smul_closedUnitBall
modified theorem integrable_exp_neg_mul_sq
modified theorem integral_cos_sq
modified theorem integral_sin_sq
modified theorem Real.rpow_add_int
modified theorem Real.rpow_add_nat
modified theorem Real.rpow_sub_int
modified theorem Real.rpow_sub_nat
modified theorem Real.arcsin_projIcc
modified theorem guard_false
modified theorem ENNReal.ofReal_pow
modified theorem Finmap.disjoint_union_left
modified theorem Finset.erase_sdiff_distrib
modified theorem Finset.erase_union_distrib
modified theorem Finset.iSup_option_toFinset
modified theorem Finsupp.card_support_eq_one
modified theorem Finset.coe_filter_univ
modified theorem Int.shiftLeft_coe_nat
modified theorem Int.cast_bit1
modified theorem AList.insert_union
modified theorem List.foldr_eta
modified theorem List.takeD_left'
modified theorem List.nodup_append
modified theorem List.lookupAll_nodup
modified theorem Matrix.dotProduct_smul
modified theorem Matrix.smul_dotProduct
modified theorem Multiset.disjoint_add_left
modified theorem Nat.dist_eq_sub_of_le_right
modified theorem Nat.add_mod_of_add_mod_lt
modified theorem Nat.nth_of_card_le
modified theorem Nat.size_shiftLeft
modified theorem Option.map₂_coe_right
modified theorem Option.map₂_comm
modified theorem Option.map₂_eq_none_iff
modified theorem Option.mem_map₂_iff
modified theorem PEquiv.mem_ofSet_self_iff
modified theorem Part.append_get_eq
modified theorem Part.inv_mem_inv
modified theorem Part.some_append_some
modified theorem Part.some_inter_some
modified theorem Rel.preimage_bot
modified theorem Rel.preimage_comp
modified theorem Semiquot.mem_bind
modified theorem Set.disjoint_singleton
modified theorem Function.invFunOn_neg
modified theorem Set.image_diff_preimage
modified theorem Set.biUnion_pair
modified theorem Sym2.eq_iff
modified theorem Sym2.other_invol
modified theorem TypeVec.const_nil
modified theorem TypeVec.eq_nilFun
modified theorem TypeVec.id_eq_nilFun
modified theorem Vector.toList_map
modified theorem hasMFDerivWithinAt_univ
modified theorem FreeGroup.invRev_invRev
modified theorem Equiv.Perm.get_toList
modified theorem Equiv.Perm.nthLe_toList
modified theorem Sylow.smul_eq_of_normal
modified theorem Finset.centroid_map
modified theorem Finsupp.supported_inter
modified theorem Finsupp.supported_union
modified theorem linearIndependent_fin_succ'
modified theorem linearIndependent_iff
modified theorem linearIndependent_option
modified theorem LinearPMap.mem_graph_iff'
modified theorem Matrix.det_neg_eq_smul
modified theorem Matrix.det_conj
modified theorem Denumerable.prod_ofNat_val
modified theorem Function.invFun_eq
modified theorem circleMap_mem_sphere
modified theorem deriv_circleMap_eq_zero_iff
modified theorem measurableSet_graph
modified theorem LowerSet.coe_iInf₂
modified theorem LowerSet.coe_iSup₂
modified theorem UpperSet.coe_iInf₂
modified theorem UpperSet.coe_iSup₂
modified theorem FdRep.char_mul_comm
modified theorem FractionalIdeal.mul_def
modified theorem IsAdjoinRoot.aequiv_root
modified theorem RatFunc.coe_smul
modified theorem IsLocalization.algEquiv_mk'
modified theorem IsFractionRing.lift_mk'
modified theorem Perfection.coeff_pow_p
modified theorem PowerBasis.degree_minpoly
modified theorem xInTermsOfW_eq
modified theorem Ordinal.type_fintype
modified theorem Ordinal.log_def
modified theorem Bornology.isBounded_iUnion
modified theorem isLindelof_range
modified theorem mem_connectedComponentIn
modified theorem Real.mem_closure_iff
modified theorem Bool_eq_iff2
modified theorem Bool_eq_iff
modified theorem Test.npowRec_zero
modified theorem Test.optiontest