Commit 2025-01-17 19:10 a4c5ecf1

View on Github →

feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)

Estimated changes

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

added theorem LieAlgebra.derivedSeriesOfIdeal_baseChange

added theorem LieAlgebra.derivedSeries_baseChange

added theorem LieAlgebra.isSolvable_tensorProduct_iff

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

added theorem Module.FaithfullyFlat.one_tmul_eq_zero_iff