From 9a7ed8cb1d2518e6110e12de15e652768ef680f0 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Tue, 22 Feb 2022 10:10:32 +0000 Subject: [PATCH] chore(algebra/lie/engel): speed up proof of Engel's theorem slightly (#12205) Local measurements using `set_option profiler true` are noisy but indicate that this speeds up elaboration of `lie_algebra.is_engelian_of_is_noetherian` by about 20% from about 10s to about 8s. --- src/algebra/lie/engel.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/algebra/lie/engel.lean b/src/algebra/lie/engel.lean index 17f98a3fec411..b27b354fdaca8 100644 --- a/src/algebra/lie/engel.lean +++ b/src/algebra/lie/engel.lean @@ -254,7 +254,8 @@ begin exact submodule.quotient.nontrivial_of_lt_top _ hK₂.lt_top, }, haveI : lie_module.is_nilpotent R K (L' ⧸ K.to_lie_submodule), { refine hK₁ _ (λ x, _), - exact module.End.is_nilpotent.mapq _ (lie_algebra.is_nilpotent_ad_of_is_nilpotent (h x)), }, + have hx := lie_algebra.is_nilpotent_ad_of_is_nilpotent (h x), + exact module.End.is_nilpotent.mapq _ hx, }, exact nontrivial_max_triv_of_is_nilpotent R K (L' ⧸ K.to_lie_submodule), }, haveI _i5 : is_noetherian R L' := is_noetherian_of_surjective L _ (linear_map.range_range_restrict (to_endomorphism R L M)),