English
There is a natural equivalence between the index set ι and the finite set of all roots, giving a labeling of allRoots P by i.
Русский
Существует естественное взаимнооднозначное соответствие между индексным множеством ι и конечным множеством всех корней, задающее нумерацию allRoots P по i.
LaTeX
$$indexEquivAllRoots : ι ≃ (allRoots P).toFinset$$
Lean4
/-- The distinguished basis carried by an `EmbeddedG2`.
In fact this is a `RootPairing.Base`. TODO Upgrade to this stronger statement. -/
def basis : Module.Basis (Fin 2) R M :=
have : LinearIndependent R ![EmbeddedG2.shortRoot P, EmbeddedG2.longRoot P] :=
by
have := pairing_long_short P
refine (IsReduced.linearIndependent_iff P).mpr ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· norm_num [h] at this
· simp only [root_eq_neg_iff] at h
norm_num [h] at this
Module.Basis.mk this (by simp)
