Merge pull request #240 from eric-wieser/rank

lean: Add missing arguments to rank
trishullab · Oct 29, 2024 · f92464e · f92464e
2 parents 975d224 + 0531062
commit f92464e
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/lean4/src/putnam_1991_a4.lean b/lean4/src/putnam_1991_a4.lean
@@ -17,6 +17,6 @@ theorem putnam_1991_a4 :
       (¬ ∃ p, MapClusterPt p atTop c) ∧
       (Summable <| fun i ↦ r i ^ 2) ∧
       (∀ L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)),
-        finrank L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
+        finrank ℝ L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
     putnam_1991_a4_solution :=
   sorry
diff --git a/lean4/src/putnam_2006_b4.lean b/lean4/src/putnam_2006_b4.lean
@@ -11,7 +11,7 @@ theorem putnam_2006_b4
 (hk : k ≤ n)
 (Z : Set (Fin n → ℝ))
 (hZ : Z = {P : Fin n → ℝ | ∀ j : Fin n, P j = 0 ∨ P j = 1})
-(hmaxeq : ∃ V : Subspace ℝ (Fin n → ℝ), Module.rank V = k ∧ (Z ∩ V).ncard = max)
-(hmaxub : ∀ V : Subspace ℝ (Fin n → ℝ), Module.rank V = k → (Z ∩ V).ncard ≤ max)
+(hmaxeq : ∃ V : Subspace ℝ (Fin n → ℝ), Module.rank ℝ V = k ∧ (Z ∩ V).ncard = max)
+(hmaxub : ∀ V : Subspace ℝ (Fin n → ℝ), Module.rank ℝ V = k → (Z ∩ V).ncard ≤ max)
 : (max = putnam_2006_b4_solution k) :=
 sorry
diff --git a/lean4/src/putnam_2008_b3.lean b/lean4/src/putnam_2008_b3.lean
@@ -13,7 +13,7 @@ theorem putnam_2008_b3
     (contains : ℝ → Prop)
     (contains_def : ∀ r, contains r ↔
       ∃ᵉ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 4))) (C ∈ A),
-        finrank A.direction = 2 ∧
+        finrank ℝ A.direction = 2 ∧
         sphere C r ∩ A ⊆ H) :
     IsGreatest contains putnam_2008_b3_solution :=
   sorry