Theorems · Theorem · linear algebra

LinearEquiv.charpoly_conj

∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Module.Finite R M₁] [inst_4 : Module.Free R M₁] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : Module.Finite R M₂] [inst_8 : Module.Free R M₂] (e : M₁ ≃ₗ[R] M₂) (φ : Module.End R M₁),
  LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ

Defined in: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Cited by: 1 results in Mathlib
Foundations: Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing AddCommGroup Module Module.Finite Module.Free AddCommGroup Module Module.Finite Module.Free

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites31

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
CommRingstatement and proof · cited by 17,173
AddCommGroupstatement and proof · cited by 12,871
Fintypeproof · cited by 7,736
Polynomialstatement and proof · cited by 5,681
Matrixproof · cited by 4,303
LinearEquivstatement and proof · cited by 3,317
Module.Basisproof · cited by 1,477
LinearEquiv.symmproof · cited by 1,461
one_smulproof · cited by 1,374

Cited by1

Results whose statement or proof uses this declaration.

LinearMap.finrank_maxGenEigenspace_zero_eqproof · cited by 2