Fixed submodules under restriction

This file supplements Mathlib's LinearMap.fixedSubmodule, the submodule of vectors fixed by a linear endomorphism, with its behaviour under restriction to an invariant submodule.

Main results

• LinearMap.fixedSubmodule_restrict: the fixed submodule of the restriction of f to an invariant submodule p is the part of the fixed submodule of f that lies in p.

theorem LinearMap.fixedSubmodule_restrict {R : Type u_1} {V : Type u_2} [Semiring R] [AddCommMonoid V] [Module R V] {f : V →ₗ[R] V} {p : Submodule R V} (hf : ∀ x ∈ p, f x ∈ p) : (f.restrict hf).fixedSubmodule = Submodule.comap p.subtype f.fixedSubmodule

If f maps a submodule p into itself, then the fixed submodule of the restriction of f to p is the part of the fixed submodule of f that lies in p.