English
The operation RestrictScalars assigns to a crystallographic root pairing a RootSystem over a subfield K on the span of the roots and coroots, coming from P.restrictScalars'.
Русский
Операция RestrictScalars задаёт корневую систему над подполем K на линейном замке порождений корней и короот, полученную через P.restrictScalars'.
LaTeX
$$$\\text{restrictScalars} : \\text{RootSystem } ι K \\bigl( \\operatorname{span}_K( \\operatorname{range}(P.root) ) \\bigr) \\bigl( \\operatorname{span}_K( \\operatorname{range}(P.coroot) ) \\bigr)$$$
Lean4
/-- Restriction of scalars for a crystallographic root pairing. -/
abbrev restrictScalars [P.IsCrystallographic] : RootSystem ι K (span K (range P.root)) (span K (range P.coroot)) :=
P.restrictScalars' K (IsValuedIn.trans P K ℤ).exists_value
