English
If B and B′ are α-rootable, then their product B × B′ is α-rootable, with root acting componentwise.
Русский
Если B и B′ являются α-узлами, то их произведение B × B′ также является α-узлом; корень действует по компонентам.
LaTeX
$$$\text{RootableBy } (B \times B') \alpha \\text{where }\text{root } (b,b') n = (\text{RootableBy.root } b n, \text{RootableBy.root } b' n)$$$
Lean4
@[to_additive]
instance rootableBy : RootableBy (B × B') β
where
root p n := (RootableBy.root p.1 n, RootableBy.root p.2 n)
root_zero _p := Prod.ext (RootableBy.root_zero _) (RootableBy.root_zero _)
root_cancel _p hn := Prod.ext (RootableBy.root_cancel _ hn) (RootableBy.root_cancel _ hn)
