Sl2update: add theorem finrank_weightSpace_eq_one_of_isIrreducible

[pion2024]

Background:

I am a 2nd year undergrad student in mathematics currently self-teaching Lie algebra and representation theory.
Before starting the formalization, I searched for related keywords on Zulip and in the GitHub issues and commits. As far as I could tell, there were no existing results or ongoing attempts before I started.

Use of AI:

I used Gemini 3.1 Pro for tactics, theorems, improvement suggestions, and error explanations. I understand and can vouch for all the modifications I have made to the file.

Limitations:

I only managed to formalize the finite-dimensional version, although the theorem also holds in the infinite-dimensional case. At this point, I only have the prerequisites (linear algebra and basics of lie algebra and representation) for the finite version, so I haven't looked deeper into the formalization of the infinite case, where the existence of a primitive vector is not guaranteed. A quick search suggests that we might need heavy tools like Casimir operators and the universal enveloping algebra, which are totally beyond my current level.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary e885514426

Import changes exceeding 2%

%	File
+23.11%	Mathlib.Algebra.Lie.Sl2

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Lie.Sl2	1467	1806	+339 (+23.11%)

Import changes for all files

Files	Import difference
4 files Mathlib.Algebra.Lie.Basis Mathlib.Algebra.Lie.Weights.IsSimple Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis	4
Mathlib.Algebra.Lie.Weights.Killing	5
Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations	7
Mathlib.Algebra.Lie.Sl2	339

---

Declarations diff

+ exists_mem_fTower_of_weightSpace_ne_bot
+ exists_primitiveVector
+ fTowerLieSubmodule
+ fTowerLieSubmodule_eq_top
+ fTowerSubmodule
+ fTowerSubmodule_eq_top
+ fTowerSubmodule_lie_e_mem
+ fTowerSubmodule_lie_f_mem
+ fTowerSubmodule_lie_h_mem
+ fTowerSubmodule_lie_mem
+ fTower_linearIndependent
+ fTower_weightSpace_independent
+ fTower_weightSpace_nontrivial
+ finrank_weightSpace_eq_one_of_isIrreducible
+ lie_e_pow_toEnd_e
+ lie_h_pow_toEnd_e
+ weightSpace

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.