Theorem: ECTate.PerfectRing.pth_root_pow_eq (ECTate/FieldTheory/PerfectClosure.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
by_cases h : ringChar R = 0
State after:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

State before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
. simp [h]
State after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

State before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
conv =>
  lhs
  rw [← Nat.mod_add_div n (ringChar R)]
State after:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ (n % ringChar R + ringChar R * (n / ringChar R)) = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)

State before:
case neg
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ¬ringChar R = 0
⊢ pth_root x ^ (n % ringChar R + ringChar R * (n / ringChar R)) = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
rw [pow_add, pow_mul, pth_root_pow_char h, mul_comm]
State after:
no goals

State before:
case pos
R : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : PerfectRing R
x : R
h : ringChar R = 0
⊢ pth_root x ^ n = x ^ (n / ringChar R) * pth_root x ^ (n % ringChar R)
Tactic:
simp [h]
State after:
no goals