Proofgold Proposition

∀ x0 . x0 ∈ octonion ⟶ ∀ x1 . x1 ∈ octonion ⟶ mul_OSNo x0 x1 ∈ octonion

type
prop

theory
HotG

name
octonion_mul_OSNo

proof
PUcEg..

Megalodon
octonion_mul_OSNo

proofgold address
TMLBM..^{octonion_mul_OSNo}

creator
28531 PrQUS../c39ac..

owner
28531 PrQUS../c39ac..

term root
1d3e8..