Theorem Submodule.coeSubtype

Modification history

2024-09-28 17:13

Mathlib/Algebra/Module/Submodule/LinearMap.lean

chore: rename Submodule.coeSubtype (#17219)

Deleted Submodule.coeSubtype View on Github →

2023-11-15 16:58

Mathlib/Algebra/Module/Submodule/Basic.lean

chore: redistribute some of the results in LinearAlgebra.Basic (#7801) …

Modified Submodule.coeSubtype View on Github →

2023-01-27 18:02

Mathlib/Algebra/Module/Submodule/Basic.lean

feat: port Algebra.Module.Submodule.Basic (#1888)

Added Submodule.coeSubtype View on Github →