Theorem Module.End.pow_restrict

Modification history

2025-04-28 09:04

Mathlib/Algebra/Module/Submodule/LinearMap.lean

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

Added Module.End.pow_restrict View on Github →