Documentation
BrauerGroup
.
Mathlib
.
LinearAlgebra
.
Matrix
.
GeneralLinearGroup
.
Basic
Search
return to top
source
Imports
Init
Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Imported by
Matrix
.
charpoly
.
similar_eq
source
theorem
Matrix
.
charpoly
.
similar_eq
{
F
:
Type
u_1}
[
Field
F
]
(
n
:
ℕ
)
(
u
:
(
Matrix
(
Fin
n
)
(
Fin
n
)
F
)
ˣ
)
(
A
B
:
Matrix
(
Fin
n
)
(
Fin
n
)
F
)
(
h
:
A
=
↑
u
*
B
*
↑
u
⁻¹
)
:
A
.
charpoly
=
B
.
charpoly