quaternionGroupZeroEquivDihedralGroupZero

English

The special case that Klein group of zero is isomorphic to the DihedralGroup of zero.

Русский

Особый случай: QuaternionGroup 0 изоморфна DihedralGroup 0.

LaTeX

$$$\text{QuaternionGroup}(0) \cong^* \text{DihedralGroup}(0)$$$

Lean4

/-- The special case that more or less by definition `QuaternionGroup 0` is isomorphic to the
infinite dihedral group. -/
def quaternionGroupZeroEquivDihedralGroupZero : QuaternionGroup 0 ≃* DihedralGroup 0
    where
  toFun
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j
  invFun
    | DihedralGroup.r j => a j
    | DihedralGroup.sr j => xa j
  left_inv := by rintro (k | k) <;> rfl
  right_inv := by rintro (k | k) <;> rfl
  map_mul' := by rintro (k | k) (l | l) <;> simp

Похожие утверждения