Identity matrix has linearly independent rows

Stream: Is there code for X?

[Martin Dvořák]

import Mathlib

theorem Matrix.one_linearIndependent {R α : Type} [Ring R] [DecidableEq α] :
    LinearIndependent R (1 : Matrix α α R) := by
  sorry

[Johan Commelin]

Please generalize to invertible matrices (-;

[Kevin Buzzard]

Is it true when alpha is empty? (not sure, genuine question, suspect not)

[Martin Dvořák]

Empty set is linearly independent. Should it be different in Lean?

[Martin Dvořák]

Johan Commelin said:

Please generalize to invertible matrices (-;

It is almost a generalization (we only discarded the infinite identity matrix):

import Mathlib

theorem Matrix.linearIndependent_of_invertible {R α : Type} [Ring R] [Fintype α] [DecidableEq α]
    {A : Matrix α α R} (hA : Invertible A) :
    LinearIndependent R A := by
  sorry

[Riccardo Brasca]

Kevin Buzzard said:

Is it true when alpha is empty? (not sure, genuine question, suspect not)

This is true by docs#linearIndependent_empty_type].

[Riccardo Brasca]

Anyway this works

import Mathlib

theorem Matrix.one_linearIndependent {R α : Type} [Ring R] [DecidableEq α] :
    LinearIndependent R (1 : Matrix α α R) := by
  rw [linearIndependent_iff]
  intro l hl
  ext j
  simpa [Finsupp.linearCombination_apply, Finsupp.sum_apply', Matrix.one_apply] using
    congr_fun hl j

[Martin Dvořák]

Thanks a lot! Will you PR it?

[Riccardo Brasca]

Feel free to do it, but I agree with Johan we want the most general version with invertible matrices (I see your point with infinite matrices, but still..)

[Riccardo Brasca]

I cannot resist to golf it

import Mathlib

open Finsupp Matrix in
theorem Matrix.one_linearIndependent {R α : Type} [Ring R] [DecidableEq α] :
    LinearIndependent R (1 : Matrix α α R) :=
  linearIndependent_iff.2 <| fun _ hl ↦ Finsupp.ext <| fun j ↦ by
    simpa [linearCombination_apply, sum_apply', one_apply] using congr_fun hl j

[Martin Dvořák]

Riccardo Brasca said:

Feel free to do it, but I agree with Johan we want the most general version with invertible matrices (I see your point with infinite matrices, but still..)

Another reason why we should have both is that

import Mathlib

variable {R α : Type} [Ring R] [Fintype α] [DecidableEq α]

theorem Matrix.linearIndependent_of_invertible {A : Matrix α α R} (hA : Invertible A) :
    LinearIndependent R A := by
  sorry -- Let's say this has been proved.

theorem Matrix.one_linearIndependent : LinearIndependent R (1 : Matrix α α R) := by
  hint

gives no useful answer.

[Martin Dvořák]

Riccardo Brasca said:

I cannot resist to golf it

import Mathlib

open Finsupp Matrix in
theorem Matrix.one_linearIndependent {R α : Type} [Ring R] [DecidableEq α] :
    LinearIndependent R (1 : Matrix α α R) :=
  linearIndependent_iff.2 <| fun _ hl ↦ Finsupp.ext <| fun j ↦ by
    simpa [linearCombination_apply, sum_apply', one_apply] using congr_fun hl j

Is Iff.2 considered idiomatic?

[Ruben Van de Velde]

It's okay, but I'd use .mpr

[Johan Commelin]

@Martin Dvořák

import Mathlib

variable {R α : Type} [Ring R] [Fintype α] [DecidableEq α]

theorem Matrix.linearIndependent_of_invertible {A : Matrix α α R} (hA : Invertible A) :
    LinearIndependent R A := by
  sorry -- Let's say this has been proved.

theorem Matrix.one_linearIndependent : LinearIndependent R (1 : Matrix α α R) := by
  apply? -- works

[Eric Wieser]

You should use IsUnit not Invertible there

[Edward van de Meent]

@loogle Matrix, LinearIndependent

[loogle]

:search: Matrix.vecMul_injective_iff, Matrix.mulVec_injective_iff, and 8 more

[Edward van de Meent]

the interesting results are in the "8 more"

[Edward van de Meent]

@loogle Matrix, LinearIndependent, IsUnit

[loogle]

:search: Matrix.linearIndependent_rows_of_isUnit, Matrix.linearIndependent_cols_of_isUnit, and 2 more

[Martin Dvořák]

Why does Matrix.linearIndependent_rows_of_isUnit talk about (fun i ↦ A i) rather than A itself?

[Martin Dvořák]

Johan Commelin said:

Martin Dvořák

import Mathlib

variable {R α : Type} [Ring R] [Fintype α] [DecidableEq α]

theorem Matrix.linearIndependent_of_invertible {A : Matrix α α R} (hA : Invertible A) :
    LinearIndependent R A := by
  sorry -- Let's say this has been proved.

theorem Matrix.one_linearIndependent : LinearIndependent R (1 : Matrix α α R) := by
  apply? -- works

It does; however, in a real-life scenario, the desired lemma will rarely come first. We should provide a lemma such that exact? hits. Then it is useful for beginners and advanced users alike.

[Johan Commelin]

Under what conditions is LinIndep R A <-> IsUnit A true? Because that would be a good simp lemma for beginners and advanced users alike.

[Riccardo Brasca]

A linear combination of the lines (or maybe of the columns, who is able to really multiply matrices) correspond to Mv for a vector v, so if M is a unit and Mv = 0 then v=0, so the lines are linearly independent (over any ring it seems).

Ops, this is already in mathlib.

[Riccardo Brasca]

(deleted)

[Kevin Buzzard]

Riccardo Brasca said:

Kevin Buzzard said:

Is it true when alpha is empty? (not sure, genuine question, suspect not)

This is true by docs#linearIndependent_empty_type].

Then I've misunderstood the mathematical claim here. Sorry for the noise.

[Johan Commelin]

Johan Commelin said:

Under what conditions is LinIndep R A <-> IsUnit A true? Because that would be a good simp lemma for beginners and advanced users alike.

I think A needs to be a division ring. For if a : A is a non-unit non-zero divisor, then ![![a]] is a counterexample.

[Johan Commelin]

(Found by Edward van de Meent)

[Riccardo Brasca]

Ah yes sure!

[Eric Wieser]

Martin Dvořák said:

Why does Matrix.linearIndependent_rows_of_isUnit talk about (fun i ↦ A i) rather than A itself?

I think for symmetry with cols, and also because passing A directly could maybe be considered defeq abuse.

[Edward van de Meent]

actually, i think the elaborator considers it a type error?

[Edward van de Meent]

nop