Powers_of_Elements_in_Group_Direct_Product
Proveddirect-productgroup-theoryproofwiki
In the group direct product G x H, the power of an element (g, h) is computed componentwise: (g, h)^n = (g^n, h^n).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Powers_of_Elements_in_Group_Direct_Product {G H : Type _} [Group G] [Group H] (g : G) (h : H) (n : ℤ) : (g, h) ^ n = (g ^ n, h ^ n) := by sorrySource