English
In a chain, the image of a prime under a divisor order is prime; the result corresponds to the second element of the chain.
Русский
В цепи образ простого элемента под отображением делителей сохраняется простота; результат соответствует второй компоненте цепи.
LaTeX
$$IsPrime (c(1))$$
Lean4
theorem eq_pow_second_of_chain_of_has_chain {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M}
(h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) (hq : q ≠ 0) : q = c 1 ^ n := by
classical
obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (@fun r => h₂) (dvd_refl q) hq
convert hi'
refine (Nat.lt_succ_iff.1 i.prop).antisymm' (Nat.le_of_succ_le_succ ?_)
calc
n + 1 = (Finset.univ : Finset (Fin (n + 1))).card := (Finset.card_fin _).symm
_ = (Finset.univ.image c).card := (Finset.card_image_iff.mpr h₁.injective.injOn).symm
_ ≤ (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card := (Finset.card_le_card ?_)
_ ≤ (Finset.univ : Finset (Fin (i + 1))).card := Finset.card_image_le
_ = i + 1 := Finset.card_fin _
intro r hr
obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hr
have := h₂.2 ⟨j, rfl⟩
rw [hi'] at this
have h := (dvd_prime_pow (show Prime (c 1) from ?_) i).1 this
· rcases h with ⟨u, hu, hu'⟩
refine Finset.mem_image.mpr ⟨⟨u, Nat.lt_succ_of_le hu⟩, Finset.mem_univ _, ?_⟩
rwa [associated_iff_eq, eq_comm] at hu'
· rw [← irreducible_iff_prime]
exact second_of_chain_is_irreducible hn h₁ (@h₂) hq
