matrix and LinearIndependent

Stream: new members

[Hbz]

import Mathlib

open Matrix

def C : Matrix (Fin 3) (Fin 3) ℝ :=
  fun i j => (i.val + 1) + (j.val + 1) - 1

variable (v₁:Fin 3 → ℝ)( v₂:Fin 3 → ℝ)( v₃ : Fin 3 → ℝ)
def V (v₁ v₂ v₃ : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ := ![v₁, v₂, v₃]

lemma V_det_ne_zero (v₁ v₂ v₃ : Fin 3 → ℝ )(h : LinearIndependent ℝ (V v₁ v₂ v₃)): det (V v₁ v₂ v₃) ≠ 0 := by
  erw[V]
  by_contra h
  erw[← exists_mulVec_eq_zero_iff_aux] at h
  rcases h with ⟨v,⟨hv1,hv2⟩⟩
  have h_lin_comb : ∑ i : Fin 3, v i • ![v₁, v₂, v₃] i = 0 := by
    ext k
    simp [Pi.zero_apply, Finset.sum_apply]
    sorry
  sorry

I don't know how to prove this seemingly obvious lemma. Why isn't this theorem, which seems so obvious to me, available in mathlib? Does it involve type conversion issues? (I'm really not good at type conversion. Alas.)

[Eric Wieser]

det (V v₁ v₂ v₃) is defeq abuse, it should be det (Matrix.of (V v₁ v₂ v₃))

[Kenny Lau]

V itself is defeq abuse

[Hbz]

Uhh,so how can i correct the def of V

[Kenny Lau]

use Matrix.of

[Kenny Lau]

actually C is also defeq abuse

[Kenny Lau]

maybe we should just seal Matrix

[Kenny Lau]

why do you have +1 +1 -1?

[Hbz]

import Mathlib

open Matrix

def C : Matrix (Fin 3) (Fin 3) ℝ :=
  fun i j => (i.val + 1) + (j.val + 1) - 1

def V (v₁ v₂ v₃ : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ := ![v₁, v₂, v₃]

lemma V_det_ne_zero (v₁ v₂ v₃ : Fin 3 → ℝ )(h : LinearIndependent ℝ (V v₁ v₂ v₃)): det (Matrix.of (V v₁ v₂ v₃)) ≠ 0 := by
  erw[V]
  by_contra h_d
  erw[← exists_mulVec_eq_zero_iff_aux] at h_d
  rcases h_d with ⟨v,⟨hv1,hv2⟩⟩
  have h_lin_comb : ∑ i : Fin 3, v i • ![v₁, v₂, v₃] i = 0 := by
    ext k
    simp [Pi.zero_apply, Finset.sum_apply]
    sorry
  sorry
lemma det_C_eq_zero : det C = 0 := by
  -- 展开为三阶行列式计算
  rw [det_fin_three C]
  -- 按定义计算每个元素
  simp only [C, Fin.val_zero, Fin.val_one, Fin.val_two,
  zero_add, Nat.cast_one, Nat.cast_add, Nat.cast_succ]
  -- 简化表达式
  ring_nf

theorem main_theorem (v₁ v₂ v₃ : Fin 3 → ℝ )(hm : LinearIndependent ℝ ![v₁, v₂, v₃]) :
    det (C * (V v₁ v₂ v₃)) = 0 := by
  -- 应用行列式乘法公式
  rw [det_mul]
  have h : det C = 0 := det_C_eq_zero
  have hV : det (V v₁ v₂ v₃) ≠ 0 := by exact V_det_ne_zero v₁ v₂ v₃ hm
  exact (mul_eq_zero_iff_right hV).mpr h

[Hbz]

I use C in the theorem

[Kenny Lau]

h is defeq abuse in the other way, which I suppose is tolerable

[Eric Wieser]

I think it helps to take a step back here and thing about what the general form of the lemma is

[Eric Wieser]

I think the one you want is genuinely missing

[Kenny Lau]

why do you know about erw...

[Eric Wieser]

docs#Matrix.linearIndependent_rows_of_det_ne_zero is the other direction

[Kenny Lau]

please don't use erw

[Kenny Lau]

@Hbz I have cleaned up your code:

import Mathlib

open Matrix

def C : Matrix (Fin 3) (Fin 3) ℝ :=
  .of fun i j => (i.val + 1) + (j.val + 1) - 1

variable (v₁ v₂ v₃ : Fin 3 → ℝ)
-- temporary def
def V (v₁ v₂ v₃ : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ :=
  .of ![v₁, v₂, v₃]

lemma det_V_ne_zero (v₁ v₂ v₃ : Fin 3 → ℝ) (h : LinearIndependent ℝ ![v₁, v₂, v₃]) :
    det (V v₁ v₂ v₃) ≠ 0 := by
  sorry

[Kenny Lau]

and yeah you shouldn't prove this if it's a missing library lemma

[Kenny Lau]

(but i guess it can still be a good exercise)

[Kenny Lau]

maybe this can be your first PR to mathlib!

[Hbz]

Kenny Lau said:

why do you know about erw...

I saw someone using it, so I gave it a try. Is there any problem with erw?

[Kenny Lau]

it's too powerful, you don't need it

[Richard Copley]

  rw [← isUnit_iff_ne_zero, ← isUnit_iff_isUnit_det]
  exact linearIndependent_rows_iff_isUnit.mp h

[Hbz]

Kenny Lau said:

it's too powerful, you don't need it

ok

[Hbz]

Richard Copley said:

  rw [← isUnit_iff_ne_zero, ← isUnit_iff_isUnit_det]
  exact linearIndependent_rows_iff_isUnit.mp h

No way, dude, you're so awesome!

[Kenny Lau]

oh wow

[Kenny Lau]

@Hbz so do you want to PR this?

[Hbz]

Of course I'd like to.

[Hbz]

but i don't know how :joy:

[Kenny Lau]

https://leanprover-community.github.io/contribute/index.html

[Hbz]

I see :ok:

[Richard Copley]

Cleaned up:

import Mathlib

open Matrix

lemma det_V_ne_zero (v₁ v₂ v₃ : Fin 3 → ℝ) (h : LinearIndependent ℝ ![v₁, v₂, v₃]) :
    det (.of ![v₁, v₂, v₃]) ≠ 0 := by
  rwa [← isUnit_iff_ne_zero, ← isUnit_iff_isUnit_det, ← linearIndependent_rows_iff_isUnit, of_row]

[Hbz]

Bro, let me ask one more thing. How did you come up with the idea of using invertible elements to prove this proposition? This kind of mathematical intuition is really stunning!

[Aaron Liu]

@loogle Matrix.det _ = 0

[loogle]

:search: Matrix.det_zero_of_row_eq, Matrix.det_updateRow_eq_zero, and 13 more

[Aaron Liu]

@loogle Matrix.det _ ≠ 0

[loogle]

:search: Matrix.linearIndependent_rows_of_det_ne_zero, Matrix.linearIndependent_cols_of_det_ne_zero, and 33 more

[Hbz]

Oh, so that's how it is. It seems I should use the robot flexibly. :joy:

[Aaron Liu]

surprisingly, it gave few useful results this time

[Aaron Liu]

but searching a lot usually gets me useful theorems eventually

[Hbz]

Aaron Liu said:

surprisingly, it gave few useful results this time

Actually, It's already a great help to be able to provide some ideas.

[Richard Copley]

Looking at what that proof proves, maybe this is better. But it is difficult to know what the most useful level of generality is.

import Mathlib

open Matrix

lemma linearIndependent_rows_iff_det_ne_zero {R α : Type*} [Field R] [Fintype α] [DecidableEq α]
    {m : Matrix α α R} : LinearIndependent R m.row ↔ m.det ≠ 0 := by
  rw [linearIndependent_rows_iff_isUnit, isUnit_iff_isUnit_det, isUnit_iff_ne_zero]

[Hbz]

Richard Copley said:

Looking at what that proof proves, maybe this is better. But it is difficult to know what the most useful level of generality is.

import Mathlib

open Matrix

lemma linearIndependent_iff_det_ne_zero {R α : Type*} [Field R] [Fintype α] [DecidableEq α]
    {m: Matrix α α R} : LinearIndependent R m.row ↔ det m ≠ 0 := by
  rw [linearIndependent_rows_iff_isUnit, isUnit_iff_isUnit_det, isUnit_iff_ne_zero]

I think this one is more universally significant.
Do we need another about
LinearIndependent R m.col ↔ det m ≠ 0

[Kenny Lau]

well I wanted Hbz to find this generalisation on their own...

[Hbz]

Kenny Lau said:

well I wanted Hbz to find this generalisation on their own...

I want to too. :smiling_face_with_tear:

[vxctyxeha]

老哥

[vxctyxeha]

@Hbz

[Hbz]

怎么出现了同胞

[vxctyxeha]

你也在做优化吗

[Hbz]

(deleted)

[vxctyxeha]

我知道你的id了 :grinning:

[Ruben Van de Velde]

This zulip instance uses English.

[Eric Wieser]

Richard Copley said:

But it is difficult to know what the most useful level of generality is.

I think we want this for a (char_zero?) integral domain, not just a field

[Richard Copley]

The lemmas I used are rather weak, in that their assumptions are strong -- mostly either DivisionRing or Field. Maybe some of them can be strengthened (a big job) or bypassed (who knows?). In the mean time, maybe there's something close to what I stated that would be nice to have. Maybe not! It's not too hard to do inline.

[Eric Wieser]

Bypassed I think is probably the approach

[Eric Wieser]

but indeed, we probably should have the lemma in mathlib with a TODO comment rather than not having it at all

[Eric Wieser]

Previous thread: #Is there code for X? > Det of family is non-zero iff linearly independent @ 💬