Theorem PiToModule.fromEnd_injective

Modification history

2023-05-21 21:36

Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

feat: port LinearAlgebra.Matrix.Charpoly.LinearMap (#4172)

Added PiToModule.fromEnd_injective View on Github →