English
Same as item 133803 but with right-hand arrangement: P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 · P.pairingIn ℤ i (long P).
Русский
То же самое, что и в пункте 133803, но правая запись: P.pairingIn ℤ i (threeShortAddTwoLong P) = P.pairingIn ℤ i (short P) + 2 · P.pairingIn ℤ i (long P).
LaTeX
$$$P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (threeShortAddTwoLong P) = P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (short P) + 2\\, P\\,\\mathrm{pairingIn}\\,\\{\\mathbb{Z}\\} i (long P)$$$
Lean4
/-- The natural labelling of `RootPairing.EmbeddedG2.allRoots`. -/
@[simps]
def indexEquivAllRoots : ι ≃ (allRoots P).toFinset :=
{ toFun i := ⟨P.root i, List.mem_toFinset.mpr <| mem_allRoots P i⟩
invFun x := (allRoots_subset_range_root P x.property).choose
left_inv i := by simp
right_inv := by
rintro ⟨x, hx⟩
simp only [Subtype.mk.injEq]
exact (allRoots_subset_range_root P hx).choose_spec }
