-- Mathlib/LinearAlgebra/Charpoly/BaseChange.lean
@[simp]
lemma LinearMap.charpoly_baseChange {R M} [CommRing R] [AddCommGroup M] [Module R M]
    [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
    (A) [CommRing A] [Algebra R A] :
    (f.baseChange A).charpoly = f.charpoly.map (algebraMap R A)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
have := (algebraMap R A).domain_nontrivial

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
nontriviality A

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
let I := Module.Free.ChooseBasisIndex R M

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Proof state:
case e_M.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
i j : I
⊢ (toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f) i j =
    ((toMatrix b b) f).map (⇑(algebraMap R A)) i j

Tactic:
simp [LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ ((toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f)).charpoly =
    (((toMatrix b b) f).map ⇑(algebraMap R A)).charpoly

Tactic:
congr 1

Result:
case e_M
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ (toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f) = ((toMatrix b b) f).map ⇑(algebraMap R A)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
let b : Basis I R M := Module.Free.chooseBasis R M

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ (baseChange A f).charpoly = Polynomial.map (algebraMap R A) f.charpoly

Tactic:
rw [← f.charpoly_toMatrix b, ← (f.baseChange A).charpoly_toMatrix (b.baseChange A),
  ← Matrix.charpoly_map]

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ ((toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f)).charpoly =
    (((toMatrix b b) f).map ⇑(algebraMap R A)).charpoly

Proof state:
case e_M
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
⊢ (toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f) = ((toMatrix b b) f).map ⇑(algebraMap R A)

Tactic:
ext i j

Result:
case e_M.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
a✝ : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Basis I R M := Module.Free.chooseBasis R M
i j : I
⊢ (toMatrix (Basis.baseChange A b) (Basis.baseChange A b)) (baseChange A f) i j =
    ((toMatrix b b) f).map (⇑(algebraMap R A)) i j