R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let A := toMatrix b b f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let b' := chooseBasis R M
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let ι' := ChooseBasisIndex R M
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let A' := toMatrix b' b' f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let e := Basis.indexEquiv b b'
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let φ := reindexLinearEquiv R R e e
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let φ₁ := reindexLinearEquiv R R e (Equiv.refl ι')
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let φ₂ := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let φ₃ := reindexLinearEquiv R R (Equiv.refl ι') e
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let P := b.toMatrix b'
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
let Q := b'.toMatrix b
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
have hPQ : C.mapMatrix (φ₁ P) ⬝ C.mapMatrix (φ₃ Q) = 1 := by
  rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul,
    reindexLinearEquiv_mul R R, Basis.toMatrix_mul_toMatrix_flip,
    reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ Matrix.charpoly (↑(toMatrix b b) f) = charpoly f
calc
  A.charpoly = (reindex e e A).charpoly := (charpoly_reindex _ _).symm
  _ = det (scalar ι' X - C.mapMatrix (φ A)) := rfl
  _ = det (scalar ι' X - C.mapMatrix (φ (P ⬝ A' ⬝ Q))) := by
    rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P ⬝ φ₂ A' ⬝ φ₃ Q)) := by
    rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
  _ = det (scalar ι' X - C.mapMatrix (φ₁ P) ⬝ C.mapMatrix A' ⬝ C.mapMatrix (φ₃ Q)) := by simp
  _ = det (scalar ι' X ⬝ C.mapMatrix (φ₁ P) ⬝ C.mapMatrix (φ₃ Q) -
        C.mapMatrix (φ₁ P) ⬝ C.mapMatrix A' ⬝ C.mapMatrix (φ₃ Q)) := by
    rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
  _ = det (C.mapMatrix (φ₁ P) ⬝ scalar ι' X ⬝ C.mapMatrix (φ₃ Q) -
        C.mapMatrix (φ₁ P) ⬝ C.mapMatrix A' ⬝ C.mapMatrix (φ₃ Q)) := by simp
  _ = det (C.mapMatrix (φ₁ P) ⬝ (scalar ι' X - C.mapMatrix A') ⬝ C.mapMatrix (φ₃ Q)) := by
    rw [← Matrix.sub_mul, ← Matrix.mul_sub]
  _ = det (C.mapMatrix (φ₁ P)) * det (scalar ι' X - C.mapMatrix A') * det (C.mapMatrix (φ₃ Q)) :=
    by rw [det_mul, det_mul]
  _ = det (C.mapMatrix (φ₁ P)) * det (C.mapMatrix (φ₃ Q)) * det (scalar ι' X - C.mapMatrix A') :=
    by ring
  _ = det (scalar ι' X - C.mapMatrix A') := by
    rw [← det_mul, hPQ, det_one, one_mul]
  _ = f.charpoly := rfl
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
⊢ ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
rw [RingHom.mapMatrix_apply, RingHom.mapMatrix_apply, ← Matrix.map_mul,
  reindexLinearEquiv_mul R R, Basis.toMatrix_mul_toMatrix_flip,
  reindexLinearEquiv_one, ← RingHom.mapMatrix_apply, RingHom.map_one]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ A)) = det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P ⬝ A' ⬝ Q)))
rw [basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ (P ⬝ A' ⬝ Q))) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P ⬝ ↑φ₂ A' ⬝ ↑φ₃ Q))
rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P ⬝ ↑φ₂ A' ⬝ ↑φ₃ Q)) =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q))
simp
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(scalar ι') X ⬝ ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q))
rw [Matrix.mul_assoc ((scalar ι') X), hPQ, Matrix.mul_one]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(scalar ι') X ⬝ ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(scalar ι') X ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q))
simp
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det
      (↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(scalar ι') X ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) -
        ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) A' ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q))
rw [← Matrix.sub_mul, ← Matrix.mul_sub]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q))
rw [det_mul, det_mul]
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') *
      det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) =
    det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
ring
no goals
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst✝ : Fintype ι
b : Basis ι R M
A : (fun x => Matrix ι ι R) f := ↑(toMatrix b b) f
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
ι' : Type v := ChooseBasisIndex R M
A' : (fun x => Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f := ↑(toMatrix b' b') f
e : ι ≃ ChooseBasisIndex R M := Basis.indexEquiv b b'
φ : Matrix ι ι R ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R := reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
P : Matrix ι (ChooseBasisIndex R M) R := Basis.toMatrix b ↑b'
Q : Matrix (ChooseBasisIndex R M) ι R := Basis.toMatrix b' ↑b
hPQ : ↑(RingHom.mapMatrix C) (↑φ₁ P) ⬝ ↑(RingHom.mapMatrix C) (↑φ₃ Q) = 1
⊢ det (↑(RingHom.mapMatrix C) (↑φ₁ P)) * det (↑(RingHom.mapMatrix C) (↑φ₃ Q)) *
      det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A') =
    det (↑(scalar ι') X - ↑(RingHom.mapMatrix C) A')
rw [← det_mul, hPQ, det_one, one_mul]