Def Submodule.compatibleMaps

Modification history

2023-10-26 10:03

Mathlib/Algebra/Module/Submodule/Map.lean

chore: move Submodule.{map,comap} to Algebra.Module.Submodule.Map (#7925)

Modified Submodule.compatibleMaps View on Github →

2023-09-01 20:13

Mathlib/LinearAlgebra/Basic.lean

chore: tidy various files (#6838)

Modified Submodule.compatibleMaps View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added Submodule.compatibleMaps View on Github →