Commit 2024-01-05 11:32 57ca1231

View on Github →

feat: refactor lemma LieModule.dualAnnihilator_ker_traceForm_le_span_weight (#9047) Also add some API for related results such as LinearMap.dualCoannihilator_range_eq_ker_flip, which is not needed here but worth having.

Estimated changes

Modified Mathlib/Algebra/Lie/Killing.lean

deleted theorem LieModule.dualAnnihilator_ker_traceForm_le_span_weight

added theorem LieModule.range_traceForm_le_span_weight

added theorem LieModule.traceForm_eq_sum_finrank_nsmul

modified theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem LinearMap.dualAnnihilator_ker_eq_range_flip

added theorem LinearMap.dualCoannihilator_range_eq_ker_flip

added theorem LinearMap.ker_dualMap_eq_dualCoannihilator_range