English
Let M be a CancelCommMonoidWithZero and p be a prime element. For a natural n ≠ 0, there exists a chain c: Fin(n+1) → Associates(M) with c(1)=p, StrictMono(c), and such that for every r, r ≤ p^n if and only if r = c(i) for some i.
Русский
Пусть M — отменимый коммутативный моноид с нулём, и p — простая элемент. Для натурального n ≠ 0 существует цепочка c: Fin(n+1) → Associates(M) такая, что c(1)=p, c строго возрастающая, и для любого r выполняется r ≤ p^n тогда и только тогда, существует i, такое что r = c(i).
LaTeX
$$$\exists c : \mathrm{Fin}(n+1) \to \mathrm{Associates}(M),\ c(1)=p \land \mathrm{StrictMono}(c) \land \forall r:\mathrm{Associates}(M),\ r \le p^n \iff \exists i:\mathrm{Fin}(n+1),\ r=c(i)$$$
Lean4
theorem exists_chain_of_prime_pow {p : Associates M} {n : ℕ} (hn : n ≠ 0) (hp : Prime p) :
∃ c : Fin (n + 1) → Associates M, c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ i, r = c i :=
by
refine ⟨fun i => p ^ (i : ℕ), ?_, fun n m h => ?_, @fun y => ⟨fun h => ?_, ?_⟩⟩
· dsimp only
rw [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt, pow_one]
exact Nat.lt_succ_of_le (Nat.one_le_iff_ne_zero.mpr hn)
·
exact
Associates.dvdNotUnit_iff_lt.mp
⟨pow_ne_zero n hp.ne_zero, p ^ (m - n : ℕ),
not_isUnit_of_not_isUnit_dvd hp.not_unit (dvd_pow dvd_rfl (Nat.sub_pos_of_lt h).ne'),
(pow_mul_pow_sub p h.le).symm⟩
· obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h
rw [associated_iff_eq] at hi
exact ⟨⟨i, Nat.lt_succ_of_le i_le⟩, hi⟩
· rintro ⟨i, rfl⟩
exact ⟨p ^ (n - i : ℕ), (pow_mul_pow_sub p (Nat.succ_le_succ_iff.mp i.2)).symm⟩
