English
For each n, the set QuaternionGroup n is equipped with a group structure.
Русский
Для каждого n множество QuaternionGroup n имеет группу как структуру.
LaTeX
$$$Group(\text{QuaternionGroup}(n))$$$
Lean4
/-- The group structure on `QuaternionGroup n`.
-/
instance : Group (QuaternionGroup n) where
mul := mul
mul_assoc := by
rintro (i | i) (j | j) (k | k) <;> simp only [(· * ·), mul] <;> ring_nf
congr
calc
-(n : ZMod (2 * n)) = 0 - n := by rw [zero_sub]
_ = 2 * n - n := by norm_cast; simp
_ = n := by ring
one := one
one_mul := by
rintro (i | i)
· exact congr_arg a (zero_add i)
· exact congr_arg xa (sub_zero i)
mul_one := by
rintro (i | i)
· exact congr_arg a (add_zero i)
· exact congr_arg xa (add_zero i)
inv := inv
inv_mul_cancel := by
rintro (i | i)
· exact congr_arg a (neg_add_cancel i)
· exact congr_arg a (sub_self (n + i))
