mathlib documentation

linear_algebra.trace

Trace of a linear map #

This file defines the trace of a linear map.

See also linear_algebra/matrix/trace.lean for the trace of a matrix.

Tags #

linear_map, trace, diagonal

def linear_map.trace_aux (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : basis ι R M) :
(M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Equations
theorem linear_map.trace_aux_def (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : M →ₗ[R] M) :
theorem linear_map.trace_aux_eq (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] {κ : Type u_1} [decidable_eq κ] [fintype κ] (b : basis ι R M) (c : basis κ R M) :
def linear_map.trace (R : Type u) [comm_ring R] (M : Type v) [add_comm_group M] [module R M] :
(M →ₗ[R] M) →ₗ[R] R

Trace of an endomorphism independent of basis.

Equations
theorem linear_map.trace_eq_matrix_trace_of_finset (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {s : finset M} (b : basis s R M) (f : M →ₗ[R] M) :

Auxiliary lemma for trace_eq_matrix_trace.

theorem linear_map.trace_eq_matrix_trace (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] {ι : Type w} [decidable_eq ι] [fintype ι] (b : basis ι R M) (f : M →ₗ[R] M) :
theorem linear_map.trace_mul_comm (R : Type u) [comm_ring R] {M : Type v} [add_comm_group M] [module R M] (f g : M →ₗ[R] M) :
(linear_map.trace R M) (f * g) = (linear_map.trace R M) (g * f)