toIdeal — Mathlib

English

The ideal of the free Lie algebra generated by Cartan relations is the Lie ideal generated by the set of all relations collected in toSet.

Русский

Идеал свободной Ли-алгебры, порожденной реляциями Картона, является лиево-идеалом, порожденным объединением множества картановых реляций.

LaTeX

$$$\\text{toIdeal } R\\; A = \\mathrm{LieSubmodule.lieSpan}\\; R\\;\\, (\\text{toSet } R A)$$$

Lean4

/-- The ideal of the free Lie algebra generated by the relations. -/
def toIdeal [DecidableEq B] : LieIdeal R (FreeLieAlgebra R (Generators B)) :=
  LieSubmodule.lieSpan R _ <| toSet R A

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