From e9560fe6b580dfcae7da55307415dd380a8b26e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= Date: Mon, 10 Aug 2026 16:15:07 +0200 Subject: [PATCH] end commit --- README.md | 6 ++++++ ZeroToLean/LearningLean/Basic.lean | 17 +++++++---------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index 0ac3904..24e5bfe 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,9 @@ +#### Important 2026-08-10 + +This project is taking too much of my time. I could realistically learn Lean and formalize most of my class results, but that would take me too much of my free time. I will continue to learn lean. But it wouldn't be trying to recreate a worst mathlib. + + + #### 2026-07-21 Note : I don't probably realize the amount of work. Hence, I might stop this project at some point. diff --git a/ZeroToLean/LearningLean/Basic.lean b/ZeroToLean/LearningLean/Basic.lean index ce12d84..9e1020e 100644 --- a/ZeroToLean/LearningLean/Basic.lean +++ b/ZeroToLean/LearningLean/Basic.lean @@ -317,15 +317,12 @@ theorem add_commutative_right (n m k: Nat) ring #check Nat.add_assoc -#check Eq.symm -#check Eq.trans -#check Nat.le_of_lt -#check Nat.le_trans -#check Nat.add_le_add_right -#check Nat.add_le_add_left -#check Nat.add_left_cancel -#check Nat.add_right_cancel +theorem add_associativity_nat (n m k: Nat) + : n + m + k = n + (m + k) := by + ring + #check Nat.mul_add -#check Nat.mul_left_comm -#check Nat.mul_right_comm +theorem mul_distribute_over_add_nat (n m k: Nat) + : n * (m + k) = n * m + n * k := by + ring end basicArithmetic