Commit 2026-04-29 11:39 031dbdd2

View on Github →

feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542) Generalise LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed to any integral domain of characteristic zero.

Estimated changes

Modified Mathlib/Algebra/Lie/CartanCriterion.lean

added theorem LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero_aux

Modified Mathlib/Algebra/Lie/TraceForm.lean

added theorem LieModule.traceForm_baseChange

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

added theorem LinearMap.BilinForm.baseChange_eq_zero_iff

added theorem LinearMap.BilinForm.baseChange_zero

Modified Mathlib/RingTheory/Flat/Basic.lean

added theorem LinearMap.baseChangeHom_injective

modified theorem Module.Flat.linearIndependent_one_tmul

added theorem Module.Flat.tensorProduct_mk_injective

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean