case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c) (i, j) = ↑b (i, j).fst • ↑c (i, j).snd
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
⊢ ↑(smul b c) ij = ↑b ij.fst • ↑c ij.snd
obtain ⟨i, j⟩ := ij
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd) = single (i, j) 1
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c) (i, j) = ↑b (i, j).fst • ↑c (i, j).snd
rw [Basis.apply_eq_iff]
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd)) (i', j') = ↑(single (i, j) 1) (i', j')
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd) = single (i, j) 1
ext ⟨i', j'⟩
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b (i, j).fst • if (i, j).snd = (i', j').snd then 1 else 0)) (i', j').fst = ↑(single (i, j) 1) (i', j')
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd)) (i', j') = ↑(single (i, j) 1) (i', j')
rw [Basis.smul_repr, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_apply,
  Finsupp.single_apply]
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b i • if j = j' then 1 else 0)) i' = ↑(single (i, j) 1) (i', j')
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b (i, j).fst • if (i, j).snd = (i', j').snd then 1 else 0)) (i', j').fst = ↑(single (i, j) 1) (i', j')
dsimp only
case mk.h.mk.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ ↑(↑b.repr (↑b i • 1)) i' = ↑(single (i, j) 1) (i', j')

case mk.h.mk.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ ↑(↑b.repr (↑b i • 0)) i' = ↑(single (i, j) 1) (i', j')
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b i • if j = j' then 1 else 0)) i' = ↑(single (i, j) 1) (i', j')
split_ifs with hi
no goals
case mk.h.mk.inl
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ ↑(↑b.repr (↑b i • 1)) i' = ↑(single (i, j) 1) (i', j')
simp [hi, Finsupp.single_apply]
no goals
case mk.h.mk.inr
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ ↑(↑b.repr (↑b i • 0)) i' = ↑(single (i, j) 1) (i', j')
simp [hi]