instZeroOfNontrivialSubtypeMemLieSubmoduleGenWeightSpaceOfNatForall

English

There exists a zero-weight instance under nontriviality hypotheses, making a canonical zero weight inhabitant when a certain generalized weight space is nontrivial.

Русский

Существует инстанс нулевого веса при ненулевой гипотезе, обеспечивающий каноническое существование нулевого веса, когда соответствующее обобщенное весовое пространство ненулево.

LaTeX

$$$\\text{Zero (Weight)} \\;\\text{under nontrivial genWeightSpace}$$$

Lean4

instance [Nontrivial (genWeightSpace M (0 : L → R))] : Zero (Weight R L M) :=
  ⟨0, fun e ↦ not_nontrivial (⊥ : LieSubmodule R L M) (e ▸ ‹_›)⟩

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