Theorem Module.End.ker_aeval_ring_hom'_unit_polynomial

Modification history

2025-10-02 09:32

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

feat(LinearAlgebra/Eigenspace/Minpoly): reduce typeclass assumptions (#29898)

Modified Module.End.ker_aeval_ring_hom'_unit_polynomial View on Github →

2023-06-12 21:52

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

feat: port LinearAlgebra.Eigenspace.Minpoly (#4861)

Added Module.End.ker_aeval_ring_hom'_unit_polynomial View on Github →