Function syntax style tweaks I didn't change every file, just the ones with important stuff instead of the garbage dump files

Changes

2 changed files (+3/-3)

• Gcd.lean
  • @@ -9,9 +9,9 @@ def N := 1000
    def A := List.range N - def sum := (A.map λ x => A.map (gcd x ·) |>.sum).sum + def sum := (A.map fun x ↦ A.map (gcd x ·) |>.sum).sum - def sumParallel := (Task.mapList List.sum <| A.map λ x => (Task.spawn λ () => A.map (gcd x ·) |>.sum)) |>.get + def sumParallel := (Task.mapList List.sum <| A.map fun x ↦ (Task.spawn fun _ ↦ A.map (gcd x ·) |>.sum)) |>.get -- #eval sum -- #eval sumParallel
• Sum.lean
  • @@ -56,7 +56,7 @@ lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3
    grind · interval_cases n <;> trivial - theorem double_sum : Tendsto (fun n : ℕ => ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by + theorem double_sum : Tendsto (fun n : ℕ ↦ ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2 n, (1 : ℝ) / (b ^ a)) atTop (𝓝 (1 : ℝ)) := by rw [atTop_basis.tendsto_iff (nhds_basis_Ioo_pos 1)] intro ε εpos simp only [true_and, Set.mem_Ici, Set.mem_Ioo]