Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Add primeDivisors as an abbreviation for n.factorization.support #7607

Closed
wants to merge 6 commits into from
Closed

feat: Add primeDivisors as an abbreviation for n.factorization.support #7607

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
dfdf251
add abbrev and rename
FLDutchmann Oct 10, 2023
4af10f6
naming
FLDutchmann Oct 10, 2023
1f45a2c
add docstring
FLDutchmann Oct 10, 2023
ba4d5d2
mem_primeDivisors and rename
FLDutchmann Oct 12, 2023
0569e5b
Merge remote-tracking branch 'origin/master' into arend/primeDivisors
FLDutchmann Oct 12, 2023
b83308e
Merge remote-tracking branch 'origin/master' into arend/primeDivisors
FLDutchmann Nov 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
117 changes: 69 additions & 48 deletions Mathlib/Data/Nat/Factorization/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,27 +122,46 @@ theorem factorization_zero : factorization 0 = 0 := by simp [factorization]
theorem factorization_one : factorization 1 = 0 := by simp [factorization]
#align nat.factorization_one Nat.factorization_one

/-- The support of `n.factorization` is exactly `n.factors.toFinset` -/
/-- The `Finset` of prime divisors of `n` -/
abbrev primeDivisors (n : ℕ) : Finset ℕ := n.factorization.support

@[simp]
theorem primeDivisors_zero : primeDivisors 0 = ∅ := by simp [primeDivisors]

@[simp]
theorem primeDivisors_one : primeDivisors 1 = ∅ := by simp [primeDivisors]

/-- The support of `n.factorization` is exactly `n.factors.toFinset` -/
theorem support_factorization {n : ℕ} : n.factorization.support = n.factors.toFinset := by
simp [factorization]
#align nat.support_factorization Nat.support_factorization

theorem factor_iff_mem_factorization {n p : ℕ} : p ∈ n.factorization.support ↔ p ∈ n.factors := by
theorem primeDivisors_eq_factors {n : ℕ} : n.primeDivisors = n.factors.toFinset := rfl

theorem primeDivisors_eq_factorization {n : ℕ} : n.primeDivisors = n.factorization.support := rfl

theorem mem_primeDivisors_iff_factor {n p : ℕ} : p ∈ n.primeDivisors ↔ p ∈ n.factors := by
simp only [support_factorization, List.mem_toFinset]
#align nat.factor_iff_mem_factorization Nat.factor_iff_mem_factorization
#align nat.factor_iff_mem_factorization Nat.mem_primeDivisors_iff_factor

theorem mem_primeDivisors {n p : ℕ} : p ∈ n.primeDivisors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sadly this can't be a simp lemma, because primeDivisors is an abbreviation and Finsupp.mem_support_iff gets to it first.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe you could instead add a simp lemma as n.factorization p ≠ 0 ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or maybe just don't use abbrev?

rw [mem_primeDivisors_iff_factor]
constructor
· refine fun h ↦ ⟨prime_of_mem_factors h, dvd_of_mem_factors h, ?_⟩
rintro rfl; simp at h
· exact fun ⟨hp, hpn, hn⟩ ↦ (mem_factors_iff_dvd hn hp).mpr hpn

theorem prime_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) : p.Prime :=
prime_of_mem_factors (factor_iff_mem_factorization.mp hp)
#align nat.prime_of_mem_factorization Nat.prime_of_mem_factorization
theorem prime_of_mem_primeDivisors {n p : ℕ} (hp : p ∈ n.primeDivisors) : p.Prime :=
mem_primeDivisors.mp hp |>.1
#align nat.prime_of_mem_factorization Nat.prime_of_mem_primeDivisors

theorem pos_of_mem_factorization {n p : ℕ} (hp : p ∈ n.factorization.support) : 0 < p :=
Prime.pos (prime_of_mem_factorization hp)
#align nat.pos_of_mem_factorization Nat.pos_of_mem_factorization
theorem pos_of_mem_primeDivisors {n p : ℕ} (hp : p ∈ n.primeDivisors) : 0 < p :=
Prime.pos (prime_of_mem_primeDivisors hp)
#align nat.pos_of_mem_factorization Nat.pos_of_mem_primeDivisors

theorem le_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ≤ n :=
le_of_mem_factors (factor_iff_mem_factorization.mp h)
#align nat.le_of_mem_factorization Nat.le_of_mem_factorization
theorem le_of_mem_primeDivisors {n p : ℕ} (h : p ∈ n.primeDivisors) : p ≤ n :=
le_of_mem_factors (mem_primeDivisors_iff_factor.mp h)
#align nat.le_of_mem_factorization Nat.le_of_mem_primeDivisors

/-! ## Lemmas characterising when `n.factorization p = 0` -/

Expand All @@ -165,7 +184,7 @@ theorem factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factori
#align nat.factorization_eq_zero_of_not_dvd Nat.factorization_eq_zero_of_not_dvd

theorem factorization_eq_zero_of_lt {n p : ℕ} (h : n < p) : n.factorization p = 0 :=
Finsupp.not_mem_support_iff.mp (mt le_of_mem_factorization (not_le_of_lt h))
Finsupp.not_mem_support_iff.mp (mt le_of_mem_primeDivisors (not_le_of_lt h))
#align nat.factorization_eq_zero_of_lt Nat.factorization_eq_zero_of_lt

@[simp]
Expand All @@ -179,7 +198,7 @@ theorem factorization_one_right (n : ℕ) : n.factorization 1 = 0 :=
#align nat.factorization_one_right Nat.factorization_one_right

theorem dvd_of_factorization_pos {n p : ℕ} (hn : n.factorization p ≠ 0) : p ∣ n :=
dvd_of_mem_factors (factor_iff_mem_factorization.1 (mem_support_iff.2 hn))
dvd_of_mem_factors (mem_primeDivisors_iff_factor.1 (mem_support_iff.2 hn))
#align nat.dvd_of_factorization_pos Nat.dvd_of_factorization_pos

theorem Prime.factorization_pos_of_dvd {n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) :
Expand Down Expand Up @@ -222,17 +241,17 @@ theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
count_append]
#align nat.factorization_mul Nat.factorization_mul

theorem factorization_mul_support {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factorization.support = a.factorization.support ∪ b.factorization.support := by
theorem primeDivisors_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).primeDivisors = a.primeDivisors ∪ b.primeDivisors := by
ext q
simp only [Finset.mem_union, factor_iff_mem_factorization]
simp only [Finset.mem_union, mem_primeDivisors_iff_factor]
exact mem_factors_mul ha hb
#align nat.factorization_mul_support Nat.factorization_mul_support
#align nat.factorization_mul_support Nat.primeDivisors_mul

/-- If a product over `n.factorization` doesn't use the multiplicities of the prime factors
then it's equal to the corresponding product over `n.factors.toFinset` -/
theorem prod_factorization_eq_prod_factors {n : ℕ} {β : Type*} [CommMonoid β] (f : ℕ → β) :
(n.factorization.prod fun p _ => f p) = ∏ p in n.factors.toFinset, f p := by
(n.factorization.prod fun p _ => f p) = ∏ p in n.primeDivisors, f p := by
apply prod_congr support_factorization
simp
#align nat.prod_factorization_eq_prod_factors Nat.prod_factorization_eq_prod_factors
Expand Down Expand Up @@ -319,7 +338,7 @@ theorem eq_factorization_iff {n : ℕ} {f : ℕ →₀ ℕ} (hn : n ≠ 0) (hf :

/-- The equiv between `ℕ+` and `ℕ →₀ ℕ` with support in the primes. -/
def factorizationEquiv : ℕ+ ≃ { f : ℕ →₀ ℕ | ∀ p ∈ f.support, Prime p } where
toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_factorization⟩
toFun := fun ⟨n, _⟩ => ⟨n.factorization, fun _ => prime_of_mem_primeDivisors⟩
invFun := fun ⟨f, hf⟩ =>
⟨f.prod _, prod_pow_pos_of_zero_not_mem_support fun H => not_prime_zero (hf 0 H)⟩
left_inv := fun ⟨_, hx⟩ => Subtype.ext <| factorization_prod_pow_eq_self hx.ne.symm
Expand Down Expand Up @@ -416,11 +435,11 @@ theorem ord_compl_mul (a b p : ℕ) : ord_compl[p] (a * b) = ord_compl[p] a * or
/-! ### Factorization and divisibility -/


theorem dvd_of_mem_factorization {n p : ℕ} (h : p ∈ n.factorization.support) : p ∣ n := by
theorem dvd_of_mem_primeDivisors {n p : ℕ} (h : p ∈ n.primeDivisors) : p ∣ n := by
rcases eq_or_ne n 0 with (rfl | hn)
· simp
simp [← mem_factors_iff_dvd hn (prime_of_mem_factorization h), factor_iff_mem_factorization.mp h]
#align nat.dvd_of_mem_factorization Nat.dvd_of_mem_factorization
simp [← mem_factors_iff_dvd hn (prime_of_mem_primeDivisors h), mem_primeDivisors_iff_factor.mp h]
#align nat.dvd_of_mem_factorization Nat.dvd_of_mem_primeDivisors

/-- A crude upper bound on `n.factorization p` -/
theorem factorization_lt {n : ℕ} (p : ℕ) (hn : n ≠ 0) : n.factorization p < n := by
Expand Down Expand Up @@ -540,7 +559,7 @@ theorem factorization_ord_compl (n p : ℕ) :
-- porting note: needed to solve side goal explicitly
rw [Finsupp.erase_of_not_mem_support]
· simp [pp]
· simp [mt prime_of_mem_factors pp]
· simp [support_factorization, mt prime_of_mem_factors pp]
ext q
rcases eq_or_ne q p with (rfl | hqp)
· simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ord_compl pp hn]
Expand Down Expand Up @@ -651,20 +670,20 @@ theorem dvd_iff_prime_pow_dvd_dvd (n d : ℕ) :
exact h p _ pp (ord_proj_dvd _ _)
#align nat.dvd_iff_prime_pow_dvd_dvd Nat.dvd_iff_prime_pow_dvd_dvd

theorem prod_prime_factors_dvd (n : ℕ) : (∏ p : ℕ in n.factors.toFinset, p) ∣ n := by
theorem prod_primeDivisors_dvd (n : ℕ) : (∏ p : ℕ in n.primeDivisors, p) ∣ n := by
by_cases hn : n = 0
· subst hn
simp
simpa [prod_factors hn] using Multiset.toFinset_prod_dvd_prod (n.factors : Multiset ℕ)
#align nat.prod_prime_factors_dvd Nat.prod_prime_factors_dvd
#align nat.prod_prime_factors_dvd Nat.prod_primeDivisors_dvd

theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) :
(gcd a b).factorization = a.factorization ⊓ b.factorization := by
let dfac := a.factorization ⊓ b.factorization
let d := dfac.prod Nat.pow
have dfac_prime : ∀ p : ℕ, p ∈ dfac.support → Prime p := by
intro p hp
have : p ∈ a.factors ∧ p ∈ b.factors := by simpa using hp
have : p ∈ a.factors ∧ p ∈ b.factors := by simpa [support_factorization] using hp
exact prime_of_mem_factors this.1
have h1 : d.factorization = dfac := prod_pow_factorization_eq_self dfac_prime
have hd_pos : d ≠ 0 := (factorizationEquiv.invFun ⟨dfac, dfac_prime⟩).2.ne'
Expand Down Expand Up @@ -692,20 +711,22 @@ theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
exact (min_add_max _ _).symm
#align nat.factorization_lcm Nat.factorization_lcm

@[to_additive sum_factors_gcd_add_sum_factors_mul]
theorem prod_factors_gcd_mul_prod_factors_mul {β : Type*} [CommMonoid β] (m n : ℕ) (f : ℕ → β) :
(m.gcd n).factors.toFinset.prod f * (m * n).factors.toFinset.prod f =
m.factors.toFinset.prod f * n.factors.toFinset.prod f := by
@[to_additive sum_primeDivisors_gcd_add_sum_primeDivisors_mul]
theorem prod_primeDivisors_gcd_mul_prod_primeDivisors_mul {β : Type*} [CommMonoid β] (m n : ℕ)
(f : ℕ → β) : (m.gcd n).primeDivisors.prod f * (m * n).primeDivisors.prod f =
m.primeDivisors.prod f * n.primeDivisors.prod f := by
rcases eq_or_ne n 0 with (rfl | hm0)
· simp
rcases eq_or_ne m 0 with (rfl | hn0)
· simp
rw [← @Finset.prod_union_inter _ _ m.factors.toFinset n.factors.toFinset, mul_comm]
rw [← @Finset.prod_union_inter _ _ m.primeDivisors n.primeDivisors, mul_comm]
congr
· apply factors_mul_toFinset <;> assumption
· simp only [← support_factorization, factorization_gcd hn0 hm0, Finsupp.support_inf]
#align nat.prod_factors_gcd_mul_prod_factors_mul Nat.prod_factors_gcd_mul_prod_factors_mul
#align nat.sum_factors_gcd_add_sum_factors_mul Nat.sum_factors_gcd_add_sum_factors_mul
· simp only [primeDivisors_eq_factorization, factorization_gcd hn0 hm0, Finsupp.support_inf]
#align nat.prod_factors_gcd_mul_prod_factors_mul Nat.prod_primeDivisors_gcd_mul_prod_primeDivisors_mul
#align nat.sum_factors_gcd_add_sum_factors_mul Nat.sum_primeDivisors_gcd_add_sum_primeDivisors_mul



theorem setOf_pow_dvd_eq_Icc_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
{ i : ℕ | i ≠ 0 ∧ p ^ i ∣ n } = Set.Icc 1 (n.factorization p) := by
Expand Down Expand Up @@ -772,18 +793,18 @@ theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b) (hpb
#align nat.factorization_eq_of_coprime_right Nat.factorization_eq_of_coprime_right

/-- The prime factorizations of coprime `a` and `b` are disjoint -/
theorem factorization_disjoint_of_coprime {a b : ℕ} (hab : Coprime a b) :
Disjoint a.factorization.support b.factorization.support := by
theorem primeDivisors_disjoint_of_coprime {a b : ℕ} (hab : Coprime a b) :
Disjoint a.primeDivisors b.primeDivisors := by
simpa only [support_factorization] using
disjoint_toFinset_iff_disjoint.mpr (coprime_factors_disjoint hab)
#align nat.factorization_disjoint_of_coprime Nat.factorization_disjoint_of_coprime
#align nat.factorization_disjoint_of_coprime Nat.primeDivisors_disjoint_of_coprime

/-- For coprime `a` and `b` the prime factorization `a * b` is the union of those of `a` and `b` -/
theorem factorization_mul_support_of_coprime {a b : ℕ} (hab : Coprime a b) :
(a * b).factorization.support = a.factorization.support ∪ b.factorization.support := by
rw [factorization_mul_of_coprime hab]
exact support_add_eq (factorization_disjoint_of_coprime hab)
#align nat.factorization_mul_support_of_coprime Nat.factorization_mul_support_of_coprime
theorem primeDivisors_mul_support_of_coprime {a b : ℕ} (hab : Coprime a b) :
(a * b).primeDivisors = a.primeDivisors ∪ b.primeDivisors := by
rw [primeDivisors_eq_factorization, factorization_mul_of_coprime hab]
exact support_add_eq (primeDivisors_disjoint_of_coprime hab)
#align nat.factorization_mul_support_of_coprime Nat.primeDivisors_mul_support_of_coprime

/-! ### Induction principles involving factorizations -/

Expand Down Expand Up @@ -869,7 +890,7 @@ theorem multiplicative_factorization {β : Type*} [CommMonoid β] (f : ℕ →
· intro a b _ _ hab ha hb hab_pos
rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
convert factorization_disjoint_of_coprime hab
convert primeDivisors_disjoint_of_coprime hab
#align nat.multiplicative_factorization Nat.multiplicative_factorization

/-- For any multiplicative function `f` with `f 1 = 1` and `f 0 = 1`,
Expand All @@ -887,7 +908,7 @@ theorem multiplicative_factorization' {β : Type*} [CommMonoid β] (f : ℕ →
simp
· intro a b _ _ hab ha hb
rw [h_mult a b hab, ha, hb, factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
exact factorization_disjoint_of_coprime hab
exact primeDivisors_disjoint_of_coprime hab
#align nat.multiplicative_factorization' Nat.multiplicative_factorization'

/-- Two positive naturals are equal if their prime padic valuations are equal -/
Expand All @@ -913,14 +934,14 @@ theorem prod_pow_prime_padicValNat (n : Nat) (hn : n ≠ 0) (m : Nat) (pr : n <
apply Finset.prod_subset_one_on_sdiff
· exact fun p hp =>
Finset.mem_filter.mpr
⟨Finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_factorization hp)),
prime_of_mem_factorization hp⟩
⟨Finset.mem_range.mpr (gt_of_gt_of_ge pr (le_of_mem_primeDivisors hp)),
prime_of_mem_primeDivisors hp⟩
· intro p hp
cases' Finset.mem_sdiff.mp hp with hp1 hp2
rw [← factorization_def n (Finset.mem_filter.mp hp1).2]
simp [Finsupp.not_mem_support_iff.mp hp2]
· intro p hp
simp [factorization_def n (prime_of_mem_factorization hp)]
simp [factorization_def n (prime_of_mem_primeDivisors hp)]
#align nat.prod_pow_prime_padic_val_nat Nat.prod_pow_prime_padicValNat

/-! ### Lemmas about factorizations of particular functions -/
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Data/Nat/Factorization/PrimePow.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ theorem isPrimePow_of_minFac_pow_factorization_eq {n : ℕ}
rcases eq_or_ne n 0 with (rfl | hn')
· simp_all
refine' ⟨_, _, (Nat.minFac_prime hn).prime, _, h⟩
rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.factor_iff_mem_factorization,
rw [pos_iff_ne_zero, ← Finsupp.mem_support_iff, Nat.mem_primeDivisors_iff_factor,
Nat.mem_factors_iff_dvd hn' (Nat.minFac_prime hn)]
apply Nat.minFac_dvd
#align is_prime_pow_of_min_fac_pow_factorization_eq isPrimePow_of_minFac_pow_factorization_eq
Expand All @@ -52,14 +52,14 @@ theorem isPrimePow_iff_factorization_eq_single {n : ℕ} :
simp_all only [Finsupp.single_eq_zero, eq_comm, Nat.factorization_zero, hk.ne']
rw [Nat.eq_pow_of_factorization_eq_single hn0 hn]
exact
⟨Nat.prime_of_mem_factorization (by simp [hn, hk.ne'] : p ∈ n.factorization.support), hk, rfl⟩
⟨Nat.prime_of_mem_primeDivisors (by simp [hn, hk.ne'] : p ∈ n.primeDivisors), hk, rfl⟩
#align is_prime_pow_iff_factorization_eq_single isPrimePow_iff_factorization_eq_single

theorem isPrimePow_iff_card_support_factorization_eq_one {n : ℕ} :
IsPrimePow n ↔ n.factorization.support.card = 1 := by
theorem isPrimePow_iff_card_primeDivisors_eq_one {n : ℕ} :
IsPrimePow n ↔ n.primeDivisors.card = 1 := by
simp_rw [isPrimePow_iff_factorization_eq_single, Finsupp.card_support_eq_one', exists_prop,
pos_iff_ne_zero]
#align is_prime_pow_iff_card_support_factorization_eq_one isPrimePow_iff_card_support_factorization_eq_one
#align is_prime_pow_iff_card_support_factorization_eq_one isPrimePow_iff_card_primeDivisors_eq_one

theorem IsPrimePow.exists_ord_compl_eq_one {n : ℕ} (h : IsPrimePow n) :
∃ p : ℕ, p.Prime ∧ ord_compl[p] n = 1 := by
Expand Down Expand Up @@ -137,7 +137,7 @@ theorem Nat.Coprime.isPrimePow_dvd_mul {n a b : ℕ} (hab : Nat.Coprime a b) (hn
rw [← Finsupp.not_mem_support_iff, ← Finsupp.not_mem_support_iff, ← not_and_or, ←
Finset.mem_inter]
intro t -- porting note: used to be `exact` below, but the definition of `∈` has changed.
simpa using (Nat.factorization_disjoint_of_coprime hab).le_bot t
simpa using (Nat.primeDivisors_disjoint_of_coprime hab).le_bot t
cases' this with h h <;> simp [h, imp_or]
#align nat.coprime.is_prime_pow_dvd_mul Nat.Coprime.isPrimePow_dvd_mul

Expand Down
7 changes: 4 additions & 3 deletions Mathlib/Data/Nat/Squarefree.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -386,9 +386,10 @@ theorem squarefree_mul_iff {m n : ℕ} :
⟨fun h => ⟨coprime_of_squarefree_mul h, (squarefree_mul $ coprime_of_squarefree_mul h).mp h⟩,
fun h => (squarefree_mul h.1).mpr h.2⟩

theorem prod_factors_toFinset_of_squarefree {n : ℕ} (hn : Squarefree n) :
∏ p in n.factors.toFinset, p = n := by
rw [List.prod_toFinset _ hn.nodup_factors, List.map_id'', Nat.prod_factors hn.ne_zero]
theorem prod_primeDivisors_of_squarefree {n : ℕ} (hn : Squarefree n) :
∏ p in n.primeDivisors, p = n := by
rw [primeDivisors_eq_factors, List.prod_toFinset _ hn.nodup_factors, List.map_id'',
Nat.prod_factors hn.ne_zero]

end Nat

Expand Down
Loading