mul_divisors_filter_prime_pow — Mathlib

English

For coprime a,b and n a prime power, the set of divisors of ab that are prime powers equals the union of divisors of a and divisors of b that are prime powers.

Русский

Для взаимно простых a и b и n — степень простого, множество делителей ab, являющихся степенями простого, совпадает с объединением множеств делителей a и делителей b, которые также являются степенями простого.

LaTeX

$$$\{ d \mid d \mid ab,\; \operatorname{IsPrimePow}(d)\} = \{ d \mid d \mid a \text{ or } d \mid b,\; \operatorname{IsPrimePow}(d)\}$$$

Lean4

theorem mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.Coprime b) :
    {d ∈ (a * b).divisors | IsPrimePow d} = {d ∈ a.divisors ∪ b.divisors | IsPrimePow d} :=
  by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp only [Nat.coprime_zero_left] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  rcases eq_or_ne b 0 with (rfl | hb)
  · simp only [Nat.coprime_zero_right] at hab
    simp [hab, Finset.filter_singleton, not_isPrimePow_one]
  ext n
  simp only [ha, hb, Finset.mem_union, Finset.mem_filter, Nat.mul_eq_zero, and_true, Ne, and_congr_left_iff,
    not_false_iff, Nat.mem_divisors, or_self_iff]
  apply hab.isPrimePow_dvd_mul

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