Commit 2026-04-23 13:30 de0e3bc3

View on Github →

perf(Algebra/Lie): un-simp two theorems (#38398)

Estimated changes

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Lie/Cochain.lean

Modified Mathlib/Algebra/Lie/Extension.lean

Modified Mathlib/Algebra/Lie/LieTheorem.lean

Modified Mathlib/Algebra/Lie/Loop.lean

Modified Mathlib/Algebra/Lie/TraceForm.lean

modified theorem LieModule.traceForm_eq_zero_of_isTrivial

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean