Theorem: DividedPowers.nilpotent_of_mem_dpIdeal (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
⊢ x ^ n = 0
Tactic:
have h_fac : (n.factorial : A) * hI.dpow n x =
  n • ((n - 1).factorial : A) * hI.dpow n x := by
  rw [nsmul_eq_mul, ← Nat.cast_mul, Nat.mul_factorial_pred (Nat.pos_of_ne_zero hn)]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ x ^ n = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ x ^ n = 0
Tactic:
rw [← factorial_mul_dpow_eq_pow hI _ _ hx, h_fac, smul_mul_assoc]
State after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ n • (↑(n - 1).factorial * hI.dpow n x) = 0

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
h_fac : ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
⊢ n • (↑(n - 1).factorial * hI.dpow n x) = 0
Tactic:
exact hnI (I.mul_mem_left ((n - 1).factorial : A) (hI.dpow_mem hn hx))
State after:
no goals

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI✝ hI : DividedPowers I
n : ℕ
hn : n ≠ 0
hnI : ∀ {y : A}, y ∈ I → n • y = 0
x : A
hx : x ∈ I
⊢ ↑n.factorial * hI.dpow n x = n • ↑(n - 1).factorial * hI.dpow n x
Tactic:
rw [nsmul_eq_mul, ← Nat.cast_mul, Nat.mul_factorial_pred (Nat.pos_of_ne_zero hn)]
State after:
no goals