Theorem: DividedPowers.RatAlgebra.dpow_eq_inv_fact_smul (DividedPowers/RatAlgebra.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = Ring.inverse ↑n ! • x ^ n
Tactic:
simp only [Ring.inverse_eq_inv']
State after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • x ^ n

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • x ^ n
Tactic:
rw [← factorial_mul_dpow_eq_pow hI n x hx]
State after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • (↑n ! * hI.dpow n x)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • (↑n ! * hI.dpow n x)
Tactic:
rw [← smul_eq_mul]
State after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • ↑n ! • hI.dpow n x

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (↑n !)⁻¹ • ↑n ! • hI.dpow n x
Tactic:
rw [← smul_assoc]
State after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Tactic:
nth_rewrite 1 [← one_smul R (hI.dpow n x)]
State after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 • hI.dpow n x = ((↑n !)⁻¹ • ↑n !) • hI.dpow n x
Tactic:
congr
State after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 = (↑n !)⁻¹ • ↑n !

State before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 = (↑n !)⁻¹ • ↑n !
Tactic:
have this_rat : ((n !) : R) = (n ! : ℚ) • (1 : R) := by
  rw [← nsmul_eq_smul_cast, nsmul_eq_mul, mul_one]
State after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = (↑n !)⁻¹ • ↑n !

State before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = (↑n !)⁻¹ • ↑n !
Tactic:
rw [this_rat, ← mul_smul]
State after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1

State before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1
Tactic:
suffices (n ! : ℚ)⁻¹ * (n !) = 1 by
  rw [this, one_smul]
State after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ (↑n !)⁻¹ * ↑n ! = 1

State before:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ (↑n !)⁻¹ * ↑n ! = 1
Tactic:
apply Rat.inv_mul_cancel
State after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ↑n ! ≠ 0

State before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ↑n ! ≠ 0
Tactic:
rw [← cast_zero, ne_eq]
State after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0

State before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬↑n ! = ↑0
Tactic:
simp only [cast_zero, cast_eq_zero]
State after:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬n ! = 0

State before:
case e_a.h
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
⊢ ¬n ! = 0
Tactic:
apply Nat.factorial_ne_zero
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ ↑n ! = ↑n ! • 1
Tactic:
rw [← nsmul_eq_smul_cast, nsmul_eq_mul, mul_one]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
this_rat : ↑n ! = ↑n ! • 1
this : (↑n !)⁻¹ * ↑n ! = 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1
Tactic:
rw [this, one_smul]
State after:
no goals