[GOAL]
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
cases (isEmpty_or_nonempty n).symm
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
cases' CharP.exists K with p hp
[GOAL]
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
letI := hp
[GOAL]
case inl.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp : CharP K p
this : CharP K p := hp
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
rcases FiniteField.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑{ val := k, property := kpos }
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ ↑{ val := k, property := kpos }
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
dsimp at hk
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
rw [hk]
[GOAL]
case inl.intro.intro.mk.intro
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ p ^ k) = charpoly M
[PROOFSTEP]
apply (frobenius_inj K[X] p).iterate k
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (↑(frobenius K[X] p))^[k] (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
repeat' rw [iterate_frobenius (R := K[X])]; rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (↑(frobenius K[X] p))^[k] (charpoly (M ^ p ^ k)) = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ p ^ k) ^ p ^ k = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = (↑(frobenius K[X] p))^[k] (charpoly M)
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ p ^ k
[PROOFSTEP]
rw [← hk]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
[PROOFSTEP]
rw [iterate_frobenius (R := K[X])]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ charpoly (M ^ Fintype.card K) ^ Fintype.card K = charpoly M ^ Fintype.card K
[PROOFSTEP]
rw [← FiniteField.expand_card]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(expand K (Fintype.card K)) (charpoly (M ^ Fintype.card K)) = charpoly M ^ Fintype.card K
[PROOFSTEP]
unfold charpoly
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(expand K (Fintype.card K)) (det (charmatrix (M ^ Fintype.card K))) = det (charmatrix M) ^ Fintype.card K
[PROOFSTEP]
rw [AlgHom.map_det, ← coe_detMonoidHom, ← (detMonoidHom : Matrix n n K[X] →* K[X]).map_pow]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑detMonoidHom (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑detMonoidHom (charmatrix M ^ Fintype.card K)
[PROOFSTEP]
apply congr_arg det
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K)) = charmatrix M ^ Fintype.card K
[PROOFSTEP]
refine' matPolyEquiv.injective _
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (Fintype.card K))) (charmatrix (M ^ Fintype.card K))) =
    ↑matPolyEquiv (charmatrix M ^ Fintype.card K)
[PROOFSTEP]
rw [AlgEquiv.map_pow, matPolyEquiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow]
[GOAL]
case inl.intro.intro.mk.intro.a
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ ↑matPolyEquiv (↑(AlgHom.mapMatrix (expand K (p ^ k))) (charmatrix (M ^ p ^ k))) = X ^ p ^ k - ↑C (M ^ p ^ k)
[PROOFSTEP]
exact (id (matPolyEquiv_eq_x_pow_sub_c (p ^ k) M) : _)
[GOAL]
case inl.intro.intro.mk.intro.a.h
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
this✝ : CharP K p := hp✝
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ Commute X (↑C M)
[PROOFSTEP]
exact (C M).commute_X
[GOAL]
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ charpoly (M ^ Fintype.card K) = charpoly M
[PROOFSTEP]
exact congr_arg _ (Subsingleton.elim _ _)
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ charpoly (M ^ p) = charpoly M
[PROOFSTEP]
have h := FiniteField.Matrix.charpoly_pow_card M
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : charpoly (M ^ Fintype.card (ZMod p)) = charpoly M
⊢ charpoly (M ^ p) = charpoly M
[PROOFSTEP]
rwa [ZMod.card] at h
[GOAL]
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
simp [Matrix.trace]
[GOAL]
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : IsEmpty n
⊢ 0 = 0 ^ Fintype.card K
[PROOFSTEP]
rw [zero_pow Fintype.card_pos]
[GOAL]
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ trace (M ^ Fintype.card K) = trace M ^ Fintype.card K
[PROOFSTEP]
rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff, FiniteField.Matrix.charpoly_pow_card,
  FiniteField.pow_card]
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
[PROOFSTEP]
have h := FiniteField.trace_pow_card M
[GOAL]
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : trace (M ^ Fintype.card (ZMod p)) = trace M ^ Fintype.card (ZMod p)
⊢ trace (M ^ p) = trace M ^ p
[PROOFSTEP]
rwa [ZMod.card] at h


[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
⊢ toMatrix e v = ↑(LinearMap.toMatrix e e) (↑(constr e ℕ) v)
[PROOFSTEP]
ext
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
v : ι → M
i✝ x✝ : ι
⊢ toMatrix e v i✝ x✝ = ↑(LinearMap.toMatrix e e) (↑(constr e ℕ) v) i✝ x✝
[PROOFSTEP]
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Basis.constr_basis]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
⊢ toMatrix (Pi.basisFun R ι) = transpose
[PROOFSTEP]
ext M i j
[GOAL]
case h.a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M✝ : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M✝
v : ι' → M✝
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
M : ι → ι → R
i j : ι
⊢ toMatrix (Pi.basisFun R ι) M i j = Mᵀ i j
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
⊢ toMatrix e ↑e = 1
[PROOFSTEP]
unfold Basis.toMatrix
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
⊢ (fun i j => ↑(↑e.repr (↑e j)) i) = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(↑e.repr (↑e j)) i = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
⊢ toMatrix e (update v j x) = updateColumn (toMatrix e v) j ↑(↑e.repr x)
[PROOFSTEP]
ext i' k
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ toMatrix e (update v j x) i' k = updateColumn (toMatrix e v) j (↑(↑e.repr x)) i' k
[PROOFSTEP]
rw [Basis.toMatrix, Matrix.updateColumn_apply, e.toMatrix_apply]
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ ↑(↑e.repr (update v j x k)) i' = if k = j then ↑(↑e.repr x) i' else ↑(↑e.repr (v k)) i'
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr x) i'
[PROOFSTEP]
rw [h, update_same j x v]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr (v k)) i'
[PROOFSTEP]
rw [update_noteq h]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
⊢ toMatrix e ↑(unitsSMul e w) = Matrix.diagonal (Units.val ∘ w)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
[PROOFSTEP]
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : DecidableEq ι
e : Basis ι R₂ M₂
w : ι → R₂ˣ
i j : ι
h : ¬i = j
⊢ toMatrix e (↑(unitsSMul e w)) i j = Matrix.diagonal (Units.val ∘ w) i j
[PROOFSTEP]
simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
⊢ ∑ i : ι, toMatrix e v i j • ↑e i = v j
[PROOFSTEP]
simp_rw [e.toMatrix_apply, e.sum_repr]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
S : Type u_9
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
⊢ vecMul (↑b) (Matrix.map (toMatrix b v) ↑(algebraMap R S)) = v
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i✝ : ι
j : ι'
S : Type u_9
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ vecMul (↑b) (Matrix.map (toMatrix b v) ↑(algebraMap R S)) i = v i
[PROOFSTEP]
simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def, sum_toMatrix_smul_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i✝ : ι
j : ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ ↑(↑(toLin v e) (toMatrix e ↑v)) (↑v i) = ↑LinearMap.id (↑v i)
[PROOFSTEP]
rw [toLin_self, id_apply, e.sum_toMatrix_smul_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
⊢ toMatrix e (v + w) = toMatrix e v + toMatrix e w
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ toMatrix e (v + w) i j = (toMatrix e v + toMatrix e w) i j
[PROOFSTEP]
change _ = _ + _
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ toMatrix e (v + w) i j = toMatrix e v i j + toMatrix e w i j
[PROOFSTEP]
rw [e.toMatrix_apply, Pi.add_apply, LinearEquiv.map_add]
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ ↑(↑e.repr (v j) + ↑e.repr (w j)) i = toMatrix e v i j + toMatrix e w i j
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ ∀ (r : R) (x : ι → M),
    AddHom.toFun
        { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) } x
[PROOFSTEP]
intro c v
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
⊢ AddHom.toFun
      { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
      (c • v) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) } v
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ AddHom.toFun
      { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
      (c • v) i j =
    (↑(RingHom.id R) c •
        AddHom.toFun
          { toFun := toMatrix e, map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
          v)
      i j
[PROOFSTEP]
dsimp only []
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ toMatrix e (c • v) i j = (↑(RingHom.id R) c • toMatrix e v) i j
[PROOFSTEP]
rw [e.toMatrix_apply, Pi.smul_apply, LinearEquiv.map_smul]
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
c : R
v : ι → M
i j : ι
⊢ ↑(c • ↑e.repr (v j)) i = (↑(RingHom.id R) c • toMatrix e v) i j
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ LeftInverse (fun m j => ∑ i : ι, m i j • ↑e i)
    {
          toAddHom :=
            { toFun := toMatrix e,
              map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
          map_smul' :=
            (_ :
              ∀ (c : R) (v : ι → M),
                AddHom.toFun
                    { toFun := toMatrix e,
                      map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                    (c • v) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      v) }.toAddHom.toFun
[PROOFSTEP]
intro v
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ (fun m j => ∑ i : ι, m i j • ↑e i)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := toMatrix e,
                map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
            map_smul' :=
              (_ :
                ∀ (c : R) (v : ι → M),
                  AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      (c • v) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        { toFun := toMatrix e,
                          map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                        v) }.toAddHom
        v) =
    v
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
j : ι
⊢ (fun m j => ∑ i : ι, m i j • ↑e i)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := toMatrix e,
                map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
            map_smul' :=
              (_ :
                ∀ (c : R) (v : ι → M),
                  AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      (c • v) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        { toFun := toMatrix e,
                          map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                        v) }.toAddHom
        v)
      j =
    v j
[PROOFSTEP]
exact e.sum_toMatrix_smul_self v j
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ Function.RightInverse (fun m j => ∑ i : ι, m i j • ↑e i)
    {
          toAddHom :=
            { toFun := toMatrix e,
              map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
          map_smul' :=
            (_ :
              ∀ (c : R) (v : ι → M),
                AddHom.toFun
                    { toFun := toMatrix e,
                      map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                    (c • v) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      v) }.toAddHom.toFun
[PROOFSTEP]
intro m
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
m : Matrix ι ι R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := toMatrix e,
              map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
          map_smul' :=
            (_ :
              ∀ (c : R) (v : ι → M),
                AddHom.toFun
                    { toFun := toMatrix e,
                      map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                    (c • v) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      v) }.toAddHom
      ((fun m j => ∑ i : ι, m i j • ↑e i) m) =
    m
[PROOFSTEP]
ext k l
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
m : Matrix ι ι R
k l : ι
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := toMatrix e,
              map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) },
          map_smul' :=
            (_ :
              ∀ (c : R) (v : ι → M),
                AddHom.toFun
                    { toFun := toMatrix e,
                      map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                    (c • v) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      { toFun := toMatrix e,
                        map_add' := (_ : ∀ (v w : ι → M), toMatrix e (v + w) = toMatrix e v + toMatrix e w) }
                      v) }.toAddHom
      ((fun m j => ∑ i : ι, m i j • ↑e i) m) k l =
    m k l
[PROOFSTEP]
simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply, LinearEquiv.apply_symm_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
⊢ ↑(toLin b' c) (Basis.toMatrix c ↑c' * ↑(toMatrix b' c') f) = ↑(toLin b' c) (↑(toMatrix b' c) f)
[PROOFSTEP]
haveI := Classical.decEq κ'
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
this : DecidableEq κ'
⊢ ↑(toLin b' c) (Basis.toMatrix c ↑c' * ↑(toMatrix b' c') f) = ↑(toLin b' c) (↑(toMatrix b' c) f)
[PROOFSTEP]
rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, id_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ ↑(toLin b c') (↑(toMatrix b' c') f * Basis.toMatrix b' ↑b) = ↑(toLin b c') (↑(toMatrix b c') f)
[PROOFSTEP]
rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, comp_id]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ Basis.toMatrix c ↑c' * ↑(toMatrix b' c') f * Basis.toMatrix b' ↑b = ↑(toMatrix b c) f
[PROOFSTEP]
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype κ
inst✝² : Fintype κ'
inst✝¹ : Fintype ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
⊢ Basis.toMatrix b₁ ↑b₂ * A = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
[PROOFSTEP]
have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype κ
inst✝² : Fintype κ'
inst✝¹ : Fintype ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : Basis.toMatrix b₁ ↑b₂ * ↑(toMatrix b₃ b₂) (↑(toLin b₃ b₂) A) = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
⊢ Basis.toMatrix b₁ ↑b₂ * A = ↑(toMatrix b₃ b₁) (↑(toLin b₃ b₂) A)
[PROOFSTEP]
rwa [LinearMap.toMatrix_toLin] at this
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
⊢ A * Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
[PROOFSTEP]
have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
this : ↑(toMatrix b₁ b₃) (↑(toLin b₁ b₃) A) * Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
⊢ A * Basis.toMatrix b₁ ↑b₂ = ↑(toMatrix b₂ b₃) (↑(toLin b₁ b₃) A)
[PROOFSTEP]
rwa [LinearMap.toMatrix_toLin] at this
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ Basis.toMatrix b ↑(Pi.basisFun R ι) * A = ↑of fun i j => ↑(↑b.repr (Aᵀ j)) i
[PROOFSTEP]
classical
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
ext i j
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply, Matrix.mulVec_stdBasis_apply, Matrix.of_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ Basis.toMatrix b ↑(Pi.basisFun R ι) * A = ↑of fun i j => ↑(↑b.repr (Aᵀ j)) i
[PROOFSTEP]
simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ ↑(toMatrix (Pi.basisFun R ι) b) (↑toLin' A) = ↑of fun i j => ↑(↑b.repr (Aᵀ j)) i
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Fintype κ'
inst✝ : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ ↑(toMatrix (Pi.basisFun R ι) b) (↑toLin' A) i j = ↑of (fun i j => ↑(↑b.repr (Aᵀ j)) i) i j
[PROOFSTEP]
rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply, Matrix.mulVec_stdBasis_apply, Matrix.of_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype κ
inst✝² : Fintype κ'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(toMatrix b b') id = Basis.toMatrix b' ↑b
[PROOFSTEP]
haveI := Classical.decEq ι'
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁹ : CommRing R₂
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁴ : Fintype ι'
inst✝³ : Fintype κ
inst✝² : Fintype κ'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
this : DecidableEq ι'
⊢ ↑(toMatrix b b') id = Basis.toMatrix b' ↑b
[PROOFSTEP]
rw [← @basis_toMatrix_mul_linearMap_toMatrix _ _ ι, toMatrix_id, Matrix.mul_one]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ toMatrix (reindex b e) v = ↑(reindexAlgEquiv R e) (toMatrix b (v ∘ ↑e))
[PROOFSTEP]
ext
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = ↑(reindexAlgEquiv R e) (toMatrix b (v ∘ ↑e)) i✝ x✝
[PROOFSTEP]
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply, Matrix.reindex_apply,
  Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply, Finsupp.mapDomain_equiv_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
⊢ toMatrix b ↑b' * toMatrix b' b'' = toMatrix b b''
[PROOFSTEP]
haveI := Classical.decEq ι
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
⊢ toMatrix b ↑b' * toMatrix b' b'' = toMatrix b b''
[PROOFSTEP]
haveI := Classical.decEq ι'
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝ : DecidableEq ι
this : DecidableEq ι'
⊢ toMatrix b ↑b' * toMatrix b' b'' = toMatrix b b''
[PROOFSTEP]
haveI := Classical.decEq ι''
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
⊢ toMatrix b ↑b' * toMatrix b' b'' = toMatrix b b''
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i✝ : ι
j✝ : ι'
N : Type u_9
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
i : ι
j : ι''
⊢ (toMatrix b ↑b' * toMatrix b' b'') i j = toMatrix b b'' i j
[PROOFSTEP]
simp only [Matrix.mul_apply, Basis.toMatrix_apply, Basis.sum_repr_mul_repr]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁶ : CommRing R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝³ : AddCommMonoid N
inst✝² : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι'
⊢ toMatrix b ↑b' * toMatrix b' ↑b = 1
[PROOFSTEP]
rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ toMatrix (reindex b e) v = submatrix (toMatrix b v) (↑e.symm) _root_.id
[PROOFSTEP]
ext
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = submatrix (toMatrix b v) (↑e.symm) _root_.id i✝ x✝
[PROOFSTEP]
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.submatrix_apply, id.def, Finsupp.mapDomain_equiv_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f✝ : M →ₗ[R] N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
⊢ toMatrix (Basis.map b f) v = toMatrix b (↑(LinearEquiv.symm f) ∘ v)
[PROOFSTEP]
ext
[GOAL]
case a.h
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f✝ : M →ₗ[R] N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
i✝ x✝ : ι
⊢ toMatrix (Basis.map b f) v i✝ x✝ = toMatrix b (↑(LinearEquiv.symm f) ∘ v) i✝ x✝
[PROOFSTEP]
simp only [Basis.toMatrix_apply, Basis.map, LinearEquiv.trans_apply, (· ∘ ·)]