English
If α and β are Primcodable, then α × β is Primcodable.
Русский
Если α и β примкодируемы, то их произведение α × β примкодируемо.
LaTeX
$$$$ \\text{Primcodable}(\\alpha \\times \\beta) \\quad\\text{whenever } \\text{Primcodable}(\\alpha) \\text{ and } \\text{Primcodable}(\\beta). $$$$
Lean4
instance prod {α β} [Primcodable α] [Primcodable β] : Primcodable (α × β) :=
⟨((casesOn' zero ((casesOn' zero .succ).comp (pair right ((Primcodable.prim β).comp left)))).comp
(pair right ((Primcodable.prim α).comp left))).of_eq
fun n => by
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
cases @decode α _ n.unpair.1; · simp
cases @decode β _ n.unpair.2 <;> simp⟩
