Theorem: Factorial.isUnit (DividedPowers/ForMathlib/AlgebraLemmas.lean)

State before:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [← map_natCast (algebraMap ℚ A)]
State after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ((algebraMap ℚ A) ↑n !)

State before:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ((algebraMap ℚ A) ↑n !)
Tactic:
apply IsUnit.map
State after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !

State before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ IsUnit ↑n !
Tactic:
rw [isUnit_iff_ne_zero]
State after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n ! ≠ 0

State before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n ! ≠ 0
Tactic:
simp only [ne_eq, Nat.cast_eq_zero]
State after:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ¬n ! = 0

State before:
case h
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ¬n ! = 0
Tactic:
exact Nat.factorial_ne_zero n
State after:
no goals