Commit 2023-01-19 10:36 1050066f

View on Github →

chore: format by line breaks with long lines (#1529) This was done semi-automatically with some regular expressions in vim in contrast to the fully automatic https://github.com/leanprover-community/mathlib4/pull/1523.

Estimated changes

modified theorem gcd_mul_left'
modified theorem gcd_pow_right_dvd_pow_gcd
modified theorem normalize_eq_normalize
modified theorem Int.pow_right_injective
modified theorem abs_add_eq_add_abs_le
modified theorem div_le_inv_mul_iff
modified theorem mul_add_mul_le_mul_add_mul'
modified theorem mul_add_mul_lt_mul_add_mul'
modified theorem range_two_mul
modified theorem IsRightRegular.pow_iff
modified theorem IsSMulRegular.of_mul
modified theorem dvd_mul_sub_mul
modified theorem Fin.predAbove_left_monotone
modified theorem Int.gcd_div
modified theorem List.prod_pos
modified theorem List.Nodup.pairwise_coe
modified theorem List.Perm.sizeOf_eq_sizeOf
modified theorem List.Perm.union_right
modified theorem List.not_mem_keys_kerase
modified theorem Nat.pow_le_iff_le_log
modified theorem Nat.findGreatest_mono_right
modified theorem Nat.not_exists_sq
modified theorem PNat.Coprime.gcd_mul
modified theorem Set.LeftInvOn.image_inter
modified theorem Set.LeftInvOn.mapsTo
modified theorem Set.piecewise_univ
modified theorem Set.image_insert_eq
modified theorem Set.projIcc_eq_right
modified theorem Set.interₛ_prod
modified theorem Set.prod_interₛ
modified theorem Set.pairwise_insert
modified theorem Set.zero_mem_smul_iff
modified theorem Setoid.sup_eq_eqvGen
modified theorem Stream'.inits_eq
modified theorem LocalEquiv.refl_prod_refl
modified theorem supᵢ_infᵢ_ge_nat_add
modified theorem csupᵢ_mono