prime_pow_coprime_prod_of_coprime_insert

English

If s is finite, i assigns exponents, and primes are included properly, the product of prime powers is coprime to p^i, hence IsRelPrime(p^{i(p)}, ∏_{p'∈s} p'^{i(p')} ).

Русский

Если s конечен и т. д., произведение степеней простых относительно p будет взаимно простым.

LaTeX

$$$IsRelPrime\\left(p^{i(p)},\\prod_{p'\\in s} p'^{i(p')}\right)$$$

Lean4

theorem prime_pow_coprime_prod_of_coprime_insert [DecidableEq α] {s : Finset α} (i : α → ℕ) (p : α) (hps : p ∉ s)
    (is_prime : ∀ q ∈ insert p s, Prime q) (is_coprime : ∀ᵉ (q ∈ insert p s) (q' ∈ insert p s), q ∣ q' → q = q') :
    IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p') :=
  by
  have hp := is_prime _ (Finset.mem_insert_self _ _)
  refine (isRelPrime_iff_no_prime_factors <| pow_ne_zero _ hp.ne_zero).mpr ?_
  intro d hdp hdprod hd
  apply hps
  replace hdp := hd.dvd_of_dvd_pow hdp
  obtain ⟨q, q_mem', hdq⟩ := hd.exists_mem_multiset_dvd hdprod
  obtain ⟨q, q_mem, rfl⟩ := Multiset.mem_map.mp q_mem'
  replace hdq := hd.dvd_of_dvd_pow hdq
  have : p ∣ q := dvd_trans (hd.irreducible.dvd_symm hp.irreducible hdp) hdq
  convert q_mem using 0
  rw [Finset.mem_val, is_coprime _ (Finset.mem_insert_self p s) _ (Finset.mem_insert_of_mem q_mem) this]

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