English
If each coordinate space B i is α-rootable, then the product space ∀ i, B i is α-rootable, with the root defined componentwise.
Русский
Если каждый пространственный фактор B_i является α-узлом, то произведение пространств ∀ i, B_i тоже является α-узлом; корень берётся по координатам.
LaTeX
$$$\text{RootableBy } (\prod_{i} B_i) \alpha \\text{with }(\text{root } x n)_i = (\text{RootableBy.root } (x_i) n)$$$
Lean4
@[to_additive]
instance rootableBy : RootableBy (∀ i, B i) β
where
root x n i := RootableBy.root (x i) n
root_zero _x := funext fun _i => RootableBy.root_zero _
root_cancel _x hn := funext fun _i => RootableBy.root_cancel _ hn
