Theorem LinearMap.iterateMapComap_le_succ

Modification history

2024-06-04 13:17
Mathlib/Algebra/Module/Submodule/IterateMapComap.lean
feat: left-Noetherian rings and commutative rings satisfy `OrzechProperty` (#13425) …
Added LinearMap.iterateMapComap_le_succView on Github →