case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ↑(toMatrix c) (comp B l r) i j = ((↑(LinearMap.toMatrix c b) l)ᵀ ⬝ ↑(toMatrix b) B ⬝ ↑(LinearMap.toMatrix c b) r) i j
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
⊢ ↑(toMatrix c) (comp B l r) = (↑(LinearMap.toMatrix c b) l)ᵀ ⬝ ↑(toMatrix b) B ⬝ ↑(LinearMap.toMatrix c b) r
ext (i j)
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ bilin B (↑l (↑c i)) (↑r (↑c j)) =
    ∑ x : n, ∑ x_1 : n, ↑(LinearMap.toMatrix c b) l x_1 i * bilin B (↑b x_1) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ↑(toMatrix c) (comp B l r) i j = ((↑(LinearMap.toMatrix c b) l)ᵀ ⬝ ↑(toMatrix b) B ⬝ ↑(LinearMap.toMatrix c b) r) i j
simp only [BilinForm.toMatrix_apply, BilinForm.comp_apply, transpose_apply, Matrix.mul_apply,
  LinearMap.toMatrix', LinearEquiv.coe_mk, sum_mul]
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ bilin B (↑l (↑c i)) (↑r (↑c j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ bilin B (↑l (↑c i)) (↑r (↑c j)) =
    ∑ x : n, ∑ x_1 : n, ↑(LinearMap.toMatrix c b) l x_1 i * bilin B (↑b x_1) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
rw [sum_comm]
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ (Finsupp.sum (↑b.repr (↑l (↑c i))) fun i xi =>
      Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => xi • yj • bilin B (↑b i) (↑b j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ bilin B (↑l (↑c i)) (↑r (↑c j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
conv_lhs => rw [← BilinForm.sum_repr_mul_repr_mul b]
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ (∑ i_1 : n, Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) i_1 • yj • bilin B (↑b i_1) (↑b j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j

case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ∀ (i : n), (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => 0 • yj • bilin B (↑b i) (↑b j)) = 0
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ (Finsupp.sum (↑b.repr (↑l (↑c i))) fun i xi =>
      Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => xi • yj • bilin B (↑b i) (↑b j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
rw [Finsupp.sum_fintype]
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) x • yj • bilin B (↑b x) (↑b j)) =
        ∑ x_1 : n, ↑(LinearMap.toMatrix c b) l x i * bilin B (↑b x) (↑b x_1) * ↑(LinearMap.toMatrix c b) r x_1 j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ (∑ i_1 : n, Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) i_1 • yj • bilin B (↑b i_1) (↑b j)) =
    ∑ y : n, ∑ x : n, ↑(LinearMap.toMatrix c b) l y i * bilin B (↑b y) (↑b x) * ↑(LinearMap.toMatrix c b) r x j
apply sum_congr rfl
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) i' • yj • bilin B (↑b i') (↑b j)) =
    ∑ x : n, ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ∀ (x : n),
    x ∈ univ →
      (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) x • yj • bilin B (↑b x) (↑b j)) =
        ∑ x_1 : n, ↑(LinearMap.toMatrix c b) l x i * bilin B (↑b x) (↑b x_1) * ↑(LinearMap.toMatrix c b) r x_1 j
rintro i' -
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∑ i_1 : n, ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) i_1 • bilin B (↑b i') (↑b i_1) =
    ∑ x : n, ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j

case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∀ (i_1 : n), ↑(↑b.repr (↑l (↑c i))) i' • 0 • bilin B (↑b i') (↑b i_1) = 0
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => ↑(↑b.repr (↑l (↑c i))) i' • yj • bilin B (↑b i') (↑b j)) =
    ∑ x : n, ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j
rw [Finsupp.sum_fintype]
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∀ (x : n),
    x ∈ univ →
      ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) x • bilin B (↑b i') (↑b x) =
        ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∑ i_1 : n, ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) i_1 • bilin B (↑b i') (↑b i_1) =
    ∑ x : n, ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j
apply sum_congr rfl
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' j' : n
⊢ ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) j' • bilin B (↑b i') (↑b j') =
    ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b j') * ↑(LinearMap.toMatrix c b) r j' j
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∀ (x : n),
    x ∈ univ →
      ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) x • bilin B (↑b i') (↑b x) =
        ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b x) * ↑(LinearMap.toMatrix c b) r x j
rintro j' -
no goals
case a.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' j' : n
⊢ ↑(↑b.repr (↑l (↑c i))) i' • ↑(↑b.repr (↑r (↑c j))) j' • bilin B (↑b i') (↑b j') =
    ↑(LinearMap.toMatrix c b) l i' i * bilin B (↑b i') (↑b j') * ↑(LinearMap.toMatrix c b) r j' j
simp only [smul_eq_mul, LinearMap.toMatrix_apply, Basis.equivFun_apply, mul_assoc, mul_comm,
  mul_left_comm]
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' i✝ : n
⊢ ↑(↑b.repr (↑l (↑c i))) i' • 0 • bilin B (↑b i') (↑b i✝) = 0
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' : n
⊢ ∀ (i_1 : n), ↑(↑b.repr (↑l (↑c i))) i' • 0 • bilin B (↑b i') (↑b i_1) = 0
intros
no goals
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i' i✝ : n
⊢ ↑(↑b.repr (↑l (↑c i))) i' • 0 • bilin B (↑b i') (↑b i✝) = 0
simp only [zero_smul, smul_zero]
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i✝ : n
⊢ (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => 0 • yj • bilin B (↑b i✝) (↑b j)) = 0
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
⊢ ∀ (i : n), (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => 0 • yj • bilin B (↑b i) (↑b j)) = 0
intros
no goals
case a.h.h
R : Type ?u.1402624
M : Type ?u.1402627
inst✝²⁰ : Semiring R
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
R₁ : Type ?u.1402663
M₁ : Type ?u.1402666
inst✝¹⁷ : Ring R₁
inst✝¹⁶ : AddCommGroup M₁
inst✝¹⁵ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹⁴ : CommSemiring R₂
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R₂ M₂
R₃ : Type ?u.1403465
M₃ : Type ?u.1403468
inst✝¹¹ : CommRing R₃
inst✝¹⁰ : AddCommGroup M₃
inst✝⁹ : Module R₃ M₃
V : Type ?u.1404056
K : Type ?u.1404059
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_5
o : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : DecidableEq n
b : Basis n R₂ M₂
M₂' : Type u_3
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
c : Basis o R₂ M₂'
inst✝ : DecidableEq o
B : BilinForm R₂ M₂
l r : M₂' →ₗ[R₂] M₂
i j : o
i✝ : n
⊢ (Finsupp.sum (↑b.repr (↑r (↑c j))) fun j yj => 0 • yj • bilin B (↑b i✝) (↑b j)) = 0
simp only [zero_smul, Finsupp.sum_zero]