Removing 'test' file and 'todoì file after exposition of my thesis to my firends

Author: giuliocaflisch

Mahler/test.lean Mahler/CurryHoward.leanMahler/test.lean renamed to Mahler/CurryHoward.lean

@@ -5,8 +5,6 @@ import Mathlib
 
 -- • Propositions as Types
 
-def x : ℕ := 1
-
 def P : Prop := 0 = 0 + 0
 def p : P := rfl
 

Mahler/NotInMathlib/ForwardDiff.lean

@@ -27,6 +27,7 @@ notation "δ_["h"]" => fwdDiff h
 
 @[simp] theorem fwdDiff_div_apply {F : Type*} [Field F] (f g : M → F) (x : M) (hx : g x ≠ 0) (hx' : g (x + h) ≠ 0) :
     δ_[h] (f / g) x = ((δ_[h] f * g - f * δ_[h] g) / (g * (g + δ_[h] g))) x := by
+
   simp only [fwdDiff,Pi.add_apply, Pi.sub_apply, Pi.mul_apply, Pi.div_apply, add_sub_cancel,
     div_sub_div _ _ hx' hx, div_eq_div_iff (mul_ne_zero hx' hx) (mul_ne_zero hx hx')]
   ring