English
The rank is witnessed by a nonzero coefficient of the characteristic polynomial of ad_R L.
Русский
Ранг модуля совпадает с ненулевым коэффициентом характеристического многочлена ад-оператора.
LaTeX
$$$$ (\\operatorname{polyCharpoly} (\\operatorname{ad} R L).toLinearMap b).\\operatorname{coeff}(\\operatorname{rank} R L) \\neq 0 $$$$
Lean4
/-- Let `L` be a Lie algebra over a nontrivial commutative ring `R`,
and assume that `L` is finite free as `R`-module.
Then the coefficients of the characteristic polynomial of `ad R L x` are polynomial in `x`.
The *rank* of `L` is the smallest `n` for which the `n`-th coefficient is not the zero polynomial.
-/
noncomputable abbrev rank : ℕ :=
LieModule.rank R L L
