Theorem LinearMap.trace_eq_zero_of_mapsTo_ne

Modification history

2024-10-09 07:18
Mathlib/Algebra/DirectSum/LinearMap.lean
feat: in a WellFoundedLT CompleteLattice, Independent sets are finite (#17525) …
Modified LinearMap.trace_eq_zero_of_mapsTo_neView on Github →
2024-08-23 14:42
Mathlib/Algebra/DirectSum/LinearMap.lean
feat(RingTheory/Artinian): make `IsArtinian` an abbreviation for `WellFoundedLT` (#15797) …
Modified LinearMap.trace_eq_zero_of_mapsTo_neView on Github →
2024-08-07 07:08
Mathlib/Algebra/DirectSum/LinearMap.lean
chore: backports for leanprover/lean4#4814 (part 23) (#15514)
Modified LinearMap.trace_eq_zero_of_mapsTo_neView on Github →
2024-03-10 21:13
Mathlib/Algebra/DirectSum/LinearMap.lean
feat: orthogonality of Lie algebra root spaces (#10879)
Added LinearMap.trace_eq_zero_of_mapsTo_neView on Github →