Theorem LinearMap.trace_restrict_eq_of_forall_mem

Modification history

2023-08-22 10:56
Mathlib/LinearAlgebra/PID.lean
feat: lemmas about Smith normal form and trace of restriction (#6666)
Added LinearMap.trace_restrict_eq_of_forall_memView on Github →