Theorem LinearMap.ker_le_of_iterateMapComap_eq_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.ker_le_of_iterateMapComap_eq_succView on Github →