dvd_of_dvd_pow — Mathlib

English

If p divides a^n, then p divides a.

Русский

Если p делит a^n, то p делит a.

LaTeX

$$p \mid a^{n} \Rightarrow p \mid a$$

Lean4

theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by
  induction n with
  | zero =>
    rw [pow_zero] at h
    have := isUnit_of_dvd_one h
    have := not_unit hp
    contradiction
  | succ n ih =>
    rw [pow_succ'] at h
    rcases dvd_or_dvd hp h with dvd_a | dvd_pow
    · assumption
    · exact ih dvd_pow

Похожие утверждения