instSubsingletonLieAlgebraRat — Mathlib

English

On a fixed ℚ-vector space L, there is at most one Lie algebra structure over ℚ; hence LieAlgebra ℚ L is subsingleton.

Русский

На заданном ℚ-векторном пространстве L существует не более одной структуры Ли над ℚ; следовательно, LieAlgebra ℚ L является дизъюнктной структурой.

LaTeX

$$Subsingleton (LieAlgebra ℚ L)$$

Lean4

instance (L : Type*) [LieRing L] : Subsingleton (LieAlgebra ℚ L) :=
  LieAlgebra.toModule_injective L |>.subsingleton

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