case a.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) i' j' = stdBasisMatrix i j 1 i' j'
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) = stdBasisMatrix i j 1
ext (i' j')
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
case a.h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
⊢ ↑(toMatrix bM bN) (↑(dualTensorHom R M N) (Basis.coord bM j ⊗ₜ[R] ↑bN i)) i' j' = stdBasisMatrix i j 1 i' j'
by_cases hij : i = i' ∧ j = j' <;>
  simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
rw [and_iff_not_or_not, Classical.not_not] at hij
no goals
case neg
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module R P
inst✝⁶ : Module R Q
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
b : Basis ι R M
m : Type u_1
n : Type u_2
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ Pi.single i (Pi.single j' 1 j) i' = 0
cases' hij with hij hij <;> simp [hij]