nonempty — Mathlib

English

If P is an irreducible, crystallographic RootPairing, then the IsG2 structure yields an embedded G2 root system via a constructive embedding P.IsG2.

Русский

Если P является неразложимым кристаллическим корневым соответствием, то структура IsG2 задаёт встроенную систему корней G2 через конструктивное вложение P.IsG2.

LaTeX

$$$ \text{embeddedG2}(P) \text{ exists with long/short roots derived from } P$$$

Lean4

theorem nonempty [P.IsG2] : Nonempty ι :=
  ⟨(IsG2.exists_pairingIn_neg_three (P := P)).choose⟩

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