Theorem AddMonoidHom.coe_toIntLinearMap_ker

Modification history

2024-02-14 03:21

Mathlib/Algebra/Module/Submodule/Ker.lean

chore: Move LinearMap.ker to a new file (#10233) …

Modified AddMonoidHom.coe_toIntLinearMap_ker View on Github →

2023-10-16 13:44

Mathlib/LinearAlgebra/Basic.lean

feat: add a Module.Finite instance for units of number field (#7412) …

Added AddMonoidHom.coe_toIntLinearMap_ker View on Github →