Def LinearEquiv.submoduleMap

Modification history

2024-02-14 03:21

Mathlib/Algebra/Module/Submodule/Map.lean

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

Modified LinearEquiv.submoduleMap View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added LinearEquiv.submoduleMap View on Github →