Theorem LinearMap.trace_eq_sum_trace_restrict'

Modification history

2024-08-07 07:08

Mathlib/Algebra/DirectSum/LinearMap.lean

chore: backports for leanprover/lean4#4814 (part 23) (#15514)

Modified LinearMap.trace_eq_sum_trace_restrict'View on Github →

2023-11-20 21:32

Mathlib/Algebra/DirectSum/LinearMap.lean

feat: if a Lie algebra has non-degenerate Killing form then its Cartan subalgebras are Abelian (#8430) …

Added LinearMap.trace_eq_sum_trace_restrict'View on Github →