Proofgold Proposition

∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ mul_HSNo x0 x1 ∈ quaternion

type
prop

theory
HotG

name
quaternion_mul_HSNo

proof
PUcEg..

Megalodon
quaternion_mul_HSNo

proofgold address
TMTWi..^{quaternion_mul_HSNo}

creator
28531 PrQUS../e367e..

owner
28531 PrQUS../e367e..

term root
c0587..