English
If gcd(|G|, n) = 1, then powCoprime h 1 = 1.
Русский
Если gcd(|G|, n) = 1, то powCoprime h 1 = 1.
LaTeX
$$powCoprime h 1 = 1$$
Lean4
/-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection -/
@[to_additive (attr := simps) /-- If `gcd(|G|,n)=1` then the smul by `n` is a bijection -/
]
noncomputable def powCoprime {G : Type*} [Group G] (h : (Nat.card G).Coprime n) : G ≃ G
where
toFun g := g ^ n
invFun g := g ^ (Nat.card G).gcdB n
left_inv
g := by
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
dsimp only at key
rwa [zpow_add, zpow_mul, zpow_mul, zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one, pow_one,
pow_card_eq_one', one_zpow, one_mul, eq_comm] at key
right_inv
g := by
have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
dsimp only at key
rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one, pow_one,
pow_card_eq_one', one_zpow, one_mul, eq_comm] at key
