n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
no goals
n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n
ring