Theorem: Nat.Prime.factorization' (LeanCourse/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean)

State before:
p : ℕ
prime_p : Prime p
⊢ ↑(Nat.factorization p) p = 1
Tactic:
rw [prime_p.factorization]
State after:
p : ℕ
prime_p : Prime p
⊢ (↑fun₀ | p => 1) p = 1

State before:
p : ℕ
prime_p : Prime p
⊢ (↑fun₀ | p => 1) p = 1
Tactic:
simp
State after:
no goals