Theorem: ZMod.pow_card_sub_one (LeanCamCombi/Mathlib/FieldTheory/Finite/Basic.lean)

State before:
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
⊢ x ^ (p - 1) = if x ≠ 0 then 1 else 0
Tactic:
split_ifs with hx
State after:
case pos
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : x ≠ 0
⊢ x ^ (p - 1) = 1

case neg
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : ¬x ≠ 0
⊢ x ^ (p - 1) = 0

State before:
case pos
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : x ≠ 0
⊢ x ^ (p - 1) = 1
Tactic:
exact pow_card_sub_one_eq_one hx
State after:
no goals

State before:
case neg
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : ¬x ≠ 0
⊢ x ^ (p - 1) = 0
Tactic:
simp [of_not_not hx, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]
State after:
no goals