instNoetherian — Mathlib

English

Lie derivations over a Noetherian Lie algebra form a Noetherian module: if R L is Noetherian, then LieDerivation R L L is Noetherian as an R-module.

Русский

Производные по Ли над Noetherian-Lie алгеброй образуют Noetherian-модуль: если R L является Noetherian, то LieDerivation R L L является Noetherian-модулем над R.

LaTeX

$$$\text{IsNoetherian } R (\text{LieDerivation } R L L)$$$

Lean4

/-- Lie derivations over a Noetherian Lie algebra form a Noetherian module. -/
instance instNoetherian [IsNoetherian R L] : IsNoetherian R (LieDerivation R L L) :=
  isNoetherian_of_linearEquiv (LinearEquiv.ofInjective _ (toLinearMapLieHom_injective R L)).symm

Похожие утверждения