Theorem Submodule.comap_injective_of_surjective

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.comap_injective_of_surjective View on Github →

2023-02-13 06:07

Mathlib/LinearAlgebra/Basic.lean

feat: port LinearAlgebra.Basic (#1979)

Added Submodule.comap_injective_of_surjective View on Github →