From d2b311cc807881d62b68b9b606ddc924da86b01f Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Sun, 24 May 2026 16:39:26 +0100 Subject: [PATCH 1/3] add one lemma --- Mathlib/LinearAlgebra/Projectivization/Independence.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Mathlib/LinearAlgebra/Projectivization/Independence.lean b/Mathlib/LinearAlgebra/Projectivization/Independence.lean index 8e265ee8a07369..fe90052dd66c82 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Independence.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Independence.lean @@ -112,4 +112,11 @@ theorem dependent_pair_iff_eq (u v : ℙ K V) : Dependent ![u, v] ↔ u = v := b theorem independent_pair_iff_ne (u v : ℙ K V) : Independent ![u, v] ↔ u ≠ v := by rw [independent_iff_not_dependent, dependent_pair_iff_eq u v] +/-- Two points are independent if and only if their underlying vectors are linearly independent. -/ +lemma independent_mk_iff_linearIndep (u v : V) (hu : u ≠ 0) (hv : v ≠ 0) : + Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v] := by + rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one] + exact ⟨fun h ↦ ⟨hv, fun a ha ↦ h ⟨a, ha⟩⟩, fun ⟨_, h⟩ ⟨a, ha⟩ ↦ h a ha⟩ + end Projectivization From 04a477391d3eafee9179feda0a0fe4df489e424a Mon Sep 17 00:00:00 2001 From: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com> Date: Mon, 25 May 2026 15:20:44 +0100 Subject: [PATCH 2/3] Update Mathlib/LinearAlgebra/Projectivization/Independence.lean Co-authored-by: Riccardo Brasca --- Mathlib/LinearAlgebra/Projectivization/Independence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Projectivization/Independence.lean b/Mathlib/LinearAlgebra/Projectivization/Independence.lean index fe90052dd66c82..e350a339bb7fed 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Independence.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Independence.lean @@ -113,7 +113,7 @@ theorem independent_pair_iff_ne (u v : ℙ K V) : Independent ![u, v] ↔ u ≠ rw [independent_iff_not_dependent, dependent_pair_iff_eq u v] /-- Two points are independent if and only if their underlying vectors are linearly independent. -/ -lemma independent_mk_iff_linearIndep (u v : V) (hu : u ≠ 0) (hv : v ≠ 0) : +lemma independent_mk_iff_linearIndep {u v : V} (hu : u ≠ 0) (hv : v ≠ 0) : Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v] := by rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2] simp only [Matrix.cons_val_zero, Matrix.cons_val_one] From 2fe22bb5465ad3a7c37b28541a45e4c6371a9cd8 Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Mon, 25 May 2026 15:23:06 +0100 Subject: [PATCH 3/3] change name --- Mathlib/LinearAlgebra/Projectivization/Independence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Projectivization/Independence.lean b/Mathlib/LinearAlgebra/Projectivization/Independence.lean index e350a339bb7fed..03bf24b66cb6ed 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Independence.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Independence.lean @@ -113,7 +113,7 @@ theorem independent_pair_iff_ne (u v : ℙ K V) : Independent ![u, v] ↔ u ≠ rw [independent_iff_not_dependent, dependent_pair_iff_eq u v] /-- Two points are independent if and only if their underlying vectors are linearly independent. -/ -lemma independent_mk_iff_linearIndep {u v : V} (hu : u ≠ 0) (hv : v ≠ 0) : +lemma independent_mk_iff_LinearIndependent {u v : V} (hu : u ≠ 0) (hv : v ≠ 0) : Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v] := by rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2] simp only [Matrix.cons_val_zero, Matrix.cons_val_one]