Theorems · Theorem · commutative algebra

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] [Module.Finite R M]
  [Module.Free R M] [IsDomain R] [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

If a linear endomorphism of a (finite, free) module M takes values in a submodule p ⊆ M, then the trace of its restriction to p is equal to its trace on M.

Defined in

Mathlib.LinearAlgebra.PID

Cited by

1 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.FiniteModule.FreeIsDomainIsPrincipalIdealRing