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

State before:
p : ℕ
prime_p : p.Prime
⊢ p.factorization p = 1
Tactic:
rw [prime_p.factorization]
State after:
p : ℕ
prime_p : p.Prime
⊢ (Finsupp.single p 1) p = 1

State before:
p : ℕ
prime_p : p.Prime
⊢ (Finsupp.single p 1) p = 1
Tactic:
simp
State after:
no goals