Matrix.one_eq_sum_single?

Stream: Is there code for X?

[Edison Xie]

import Mathlib

lemma Matrix.one_eq_sum_single {R ι : Type*} [Ring R] [Fintype ι] [DecidableEq ι] :
    (1 : Matrix ι ι R) = ∑ i : ι, single i i 1 := by
  rw [Matrix.matrix_eq_sum_single 1]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  rw [Finset.sum_eq_single i (fun b _ hb ↦ by simp [Ne.symm hb]) (by simp)]
  simp

Do we have this in mathlib?

[Edison Xie]

Pining @Eric Wieser

[Eric Wieser]

Probably not, I'd expect a version for diagonal too

[Edison Xie]

should I PR these then?

lemma Matrix.one_eq_sum_single {ι : Type*} [Fintype ι] [DecidableEq ι] :
    (1 : Matrix ι ι R) = ∑ i : ι, single i i 1 := by
  rw [Matrix.matrix_eq_sum_single 1]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  rw [Finset.sum_eq_single i (fun b _ hb ↦ by simp [Ne.symm hb]) (by simp)]
  simp

lemma Matrix.diagonal_eq_sum_single {ι : Type*} [Fintype ι] [DecidableEq ι]
    (f : ι → R) : Matrix.diagonal f = ∑ i : ι, single i i (f i) := by
  rw [Matrix.matrix_eq_sum_single (Matrix.diagonal f)]
  refine Finset.sum_congr rfl fun i _ ↦ ?_
  rw [Finset.sum_eq_single i (fun b _ hb ↦ by simp [Ne.symm hb]) (by simp)]
  simp

[Kenny Lau]

you should switch them and prove one from diag...

[Kenny Lau]

@Edison Xie :cooking:

import Mathlib

lemma Matrix.diagonal_eq_sum_single {R : Type*} [AddCommMonoid R] {ι : Type*} [Fintype ι] [DecidableEq ι]
    (f : ι → R) : Matrix.diagonal f = ∑ i : ι, single i i (f i) := ext fun j k ↦ by
  rw [sum_apply, diagonal_apply, Finset.sum_eq_single j] <;> simp +contextual [single]

lemma Matrix.one_eq_sum_single {R : Type*} [AddCommMonoidWithOne R] {ι : Type*} [Fintype ι] [DecidableEq ι] :
    (1 : Matrix ι ι R) = ∑ i : ι, single i i 1 :=
  diagonal_eq_sum_single _

#min_imports

[Edison Xie]

why don't we have stuff like single_def and single_apply? Should we really be unfolding the definition every time? Should I add those as well?

[Edison Xie]

I could only find single_apply_of_ne and single_apply_of_same

[Kenny Lau]

I agree that we shouldn't rely on definitional unfolding, but I also think that we can also get a long way if loogle can also look under definition

[Edison Xie]

Kenny Lau said:

Edison Xie :cooking:

import Mathlib

lemma Matrix.diagonal_eq_sum_single {R : Type*} [AddCommMonoid R] {ι : Type*} [Fintype ι] [DecidableEq ι]
    (f : ι → R) : Matrix.diagonal f = ∑ i : ι, single i i (f i) := ext fun j k ↦ by
  rw [sum_apply, diagonal_apply, Finset.sum_eq_single j] <;> simp +contextual [single]

lemma Matrix.one_eq_sum_single {R : Type*} [AddCommMonoidWithOne R] {ι : Type*} [Fintype ι] [DecidableEq ι] :
    (1 : Matrix ι ι R) = ∑ i : ι, single i i 1 :=
  diagonal_eq_sum_single _

#min_imports

#31637