Def Submodule.orderIsoMapComapOfBijective

Modification history

2025-12-27 09:40

Mathlib/Algebra/Module/Submodule/Map.lean

chore(*): restrict operations to `LinearMap`s (#33241) …

Modified Submodule.orderIsoMapComapOfBijective View on Github →

2024-03-05 01:29

Mathlib/Algebra/Module/Submodule/Map.lean

feat: sum and product of commuting semisimple endomorphisms (#10808) …

Added Submodule.orderIsoMapComapOfBijective View on Github →