coe_zero_iff_zero — Mathlib

English

Let x be an element of a Lie subalgebra L'. Then (x : L) = 0 in L if and only if x = 0 in L'.

Русский

Пусть x принадлежит L'. Тогда (x : L) = 0 в L тогда и только если x = 0 в L'.

LaTeX

$$$$\forall {R : Type u} {L : Type v} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L] (L' : \text{LieSubalgebra } R L)\ (x : L'),\ (x : L) = 0 \iff x = 0.$$$$

Lean4

theorem coe_zero_iff_zero (x : L') : (x : L) = 0 ↔ x = 0 :=
  (ext_iff L' x 0).symm

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