l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P (∑ x in Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.fst x.snd (M x.fst x.snd))
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P M
rw [matrix_eq_sum_std_basis M, ← Finset.sum_product']
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ ∀ (x : m × n), x ∈ Finset.univ ×ˢ Finset.univ → P (stdBasisMatrix x.fst x.snd (M x.fst x.snd))
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P (∑ x in Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.fst x.snd (M x.fst x.snd))
apply Finset.sum_induction _ _ h_add h_zero
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.fst x✝.snd (M x✝.fst x✝.snd))
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ ∀ (x : m × n), x ∈ Finset.univ ×ˢ Finset.univ → P (stdBasisMatrix x.fst x.snd (M x.fst x.snd))
intros
no goals
l : Type ?u.17264
m : Type u_1
n : Type u_2
R : Type ?u.17273
α : Type u_3
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.fst x✝.snd (M x✝.fst x✝.snd))
apply h_std_basis