LinearMap.trace_restrict_eq_of_forall_mem

theorem LinearMap.trace_restrict_eq_of_forall_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Module.Finite R M] [inst_4 : Module.Free R M] [inst_5 : IsDomain R] [inst_6 : IsPrincipalIdealRing R] (p : Submodule R M) (f : M →ₗ[R] M) (hf : ∀ (x : M), f x ∈ p) (hf' : optParam (∀ x ∈ p, f x ∈ p) ⋯), (LinearMap.trace R ↥p) (f.restrict hf') = (LinearMap.trace R M) f

This theorem states that for a given commutative ring `R`, and a module `M` over `R` which is both finite and free, if a linear endomorphism `f` of `M` always maps its elements to a submodule `p` of `M` (i.e., for every element `x` of `M`, `f(x)` is an element of `p`), then the trace of the restriction of `f` to `p` is equal to the trace of `f` on `M`. Here, we assume that `R` is a domain and a principal ideal ring, and the condition `f(x) ∈ p` for every `x` in `p` is optionally given. The trace of an endomorphism here is defined independent of the basis.

More concisely: If `R` is a commutative domain and principal ideal ring, and `M` is a finite free `R`-module, when an endomorphism `f` of `M` maps every element of the submodule `p` of `M` to itself, then the trace of `f` on `M` equals the trace of `f` restricted to `p`.