Commit 2023-07-19 05:37 12343aa5

View on Github →

chore: cleanup whitespace (#5988) Grepping for [^ .:{-] [^ :] and reviewing the results. Once I started I couldn't stop. :-)

Estimated changes

modified def AddMonoidHom.mulOp
modified theorem NonUnitalAlgHom.coe_mk
modified theorem LieModuleHom.coe_comp
modified def Random.randBound
modified theorem Finset.coe_smul_finset
modified theorem List.filter_true
modified theorem map_ofNat
modified theorem Nat.choose_le_pow
modified def Ordnode.repr
modified theorem Polynomial.map_roots_le
modified theorem Set.ordConnected_biInter
modified theorem Stream'.eq_of_bisim
modified theorem Equivalence.transitive
modified def Ideal.radical
modified theorem Ordinal.mul_add_mod_self
modified def Simps.defaultfindArgs
modified theorem eq_irreducibleComponent
modified theorem Test.bar2_works
modified theorem Test.bar3_works