Theorem Module.End.iterate_surjective

Modification history

2025-04-28 09:04

Mathlib/Algebra/Module/LinearMap/End.lean

chore: move `Module.End`-related decls to the `Module.End` namespace (#23705) …

Added Module.End.iterate_surjective View on Github →