rw [unit_l]
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑unit * ↑unit = { f := -5, g := -14, h := -4 }
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ { f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 } = { f := -5, g := -14, h := -4 }