weird FTA based lemma

Stream: general

[Frederick Pu]

I'm trying to prove the following lemma does anyone know a simple way to prove it or if it's already in mathlib?

(a p : Nat)
(hp : p.Prime)
⊢ (orderOf a / p ^ a.factorization p).factorization p = 0

[Aaron Liu]

why do you want to prove this

[Aaron Liu]

this doesn't seem like something that would normally be wanted to be proved

[Aaron Liu]

import Mathlib

example (a p : Nat)
    -- unused variable `hp`, which means my proof didn't use the fact that `p` is prime
    (hp : p.Prime) :
    (orderOf a / p ^ a.factorization p).factorization p = 0 := by
  by_cases ha : a = 1
  · simp [ha]
  · have hn : ¬IsOfFinOrder a := by
      apply mt IsOfFinOrder.isUnit
      simp [ha]
    simp [orderOf_eq_zero hn]

[Frederick Pu]

I meant a instead of orderOf a

[Aaron Liu]

that makes a bit more sense

[Aaron Liu]

import Mathlib

example (a p : Nat) :
    (a / p ^ a.factorization p).factorization p = 0 := by
  by_cases hp : p.Prime
  · have ha : p ^ a.factorization p ∣ a :=
      -- found by `exact?` (can we rename this?)
      Nat.ordProj_dvd a p
    rw [Nat.factorization_div ha]
    simp [hp]
  · simp [hp]

[Frederick Pu]

thx!