Theorem: l1_2_23 (AlgebraI/Subgroups.lean)

State before:
n : ℕ+
x : ℤ
h : IsCoprime x ↑↑n
⊢ x ^ φ ↑n ≡ 1 [ZMOD ↑↑n]
Tactic:
rw [← CharP.intCast_eq_intCast (ZMod n), Int.cast_pow, Int.cast_one, ←
  coe_unitOfIsCoprime' _ h, ← Units.val_pow_eq_pow_val, Units.val_eq_one, ← ZMod.pow_totient' _]
State after:
no goals