have h1 : ((unit * unit : ℤθˣ) : ℤθ) = ((unit : ℤθˣ) : ℤθ) * ((unit : ℤθˣ) : ℤθ) := by rfl
a b c : ℤθ
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }
a b c : ℤθ
h1 : ↑(unit * unit) = ↑unit * ↑unit
⊢ ↑(unit * unit) = { f := -5, g := -14, h := -4 }