lieAlgebra_ext — Mathlib

English

Two elements of the direct sum are equal if all their component Lie algebra coordinates are equal.

Русский

Два элемента прямой суммы равны, если их компоненты в каждой L_i совпадают.

LaTeX

$$lieAlgebra_ext {x y : ⨁ i, L i} (h : ∀ i, lieAlgebraComponent R ι L i x = lieAlgebraComponent R ι L i y) : x = y.$$

Lean4

@[ext (iff := false)]
theorem lieAlgebra_ext {x y : ⨁ i, L i} (h : ∀ i, lieAlgebraComponent R ι L i x = lieAlgebraComponent R ι L i y) :
    x = y :=
  DFinsupp.ext h

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