Def Submodule.negOrderIso

Modification history

2024-05-17 19:31

Mathlib/Algebra/Module/Submodule/Pointwise.lean

style: remove all isolated `where` (#12991)

Modified Submodule.negOrderIso View on Github →

2023-02-14 23:47

Mathlib/Algebra/Module/Submodule/Pointwise.lean

feat: port Algebra.Module.Submodule.Pointwise (#2285)

Added Submodule.negOrderIso View on Github →