From dfdf25110a599a85d7cbca1e308eca92861ce7bb Mon Sep 17 00:00:00 2001 From: Arend Mellendijk Date: Tue, 10 Oct 2023 16:10:54 +0200 Subject: [PATCH 1/4] add abbrev and rename --- Mathlib/Data/Nat/Factorization/Basic.lean | 99 ++++++++++--------- Mathlib/Data/Nat/Factorization/PrimePow.lean | 12 +-- Mathlib/Data/Nat/Squarefree.lean | 5 +- Mathlib/Data/Nat/Totient.lean | 28 +++--- Mathlib/GroupTheory/Exponent.lean | 2 +- Mathlib/GroupTheory/Nilpotent.lean | 8 +- Mathlib/GroupTheory/Sylow.lean | 16 +-- .../Cyclotomic/PrimitiveRoots.lean | 2 +- 8 files changed, 92 insertions(+), 80 deletions(-) diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index b6c3a84419c7a..69e5f5bef3583 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -122,27 +122,38 @@ 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` -/ +abbrev primeDivisors (n : ℕ) := 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 factor_iff_mem_primeDivisors {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.factor_iff_mem_primeDivisors -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 := + prime_of_mem_factors (factor_iff_mem_primeDivisors.mp hp) +#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 (factor_iff_mem_primeDivisors.mp h) +#align nat.le_of_mem_factorization Nat.le_of_mem_primeDivisors /-! ## Lemmas characterising when `n.factorization p = 0` -/ @@ -165,7 +176,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] @@ -179,7 +190,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 (factor_iff_mem_primeDivisors.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) : @@ -222,17 +233,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, factor_iff_mem_primeDivisors] 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 @@ -319,7 +330,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 @@ -416,11 +427,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), factor_iff_mem_primeDivisors.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 @@ -540,7 +551,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] @@ -651,12 +662,12 @@ 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 @@ -664,7 +675,7 @@ theorem factorization_gcd {a b : ℕ} (ha_pos : a ≠ 0) (hb_pos : b ≠ 0) : 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' @@ -694,16 +705,16 @@ theorem factorization_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : @[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 + (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] + · simp only [primeDivisors_eq_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 @@ -772,18 +783,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 -/ @@ -869,7 +880,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`, @@ -887,7 +898,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 -/ @@ -913,14 +924,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 -/ diff --git a/Mathlib/Data/Nat/Factorization/PrimePow.lean b/Mathlib/Data/Nat/Factorization/PrimePow.lean index 542eef569f8f0..3473c20ab3010 100644 --- a/Mathlib/Data/Nat/Factorization/PrimePow.lean +++ b/Mathlib/Data/Nat/Factorization/PrimePow.lean @@ -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.factor_iff_mem_primeDivisors, 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 @@ -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 @@ -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 diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 2efd9b9c22eab..908df7f1e3bb5 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -387,8 +387,9 @@ theorem squarefree_mul_iff {m n : ℕ} : 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] + ∏ 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 diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index 5ccac5e1c233d..be73b87648557 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -286,12 +286,12 @@ theorem totient_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) : apply Finsupp.prod_congr _ intro p hp have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp) - rw [totient_prime_pow (prime_of_mem_factorization hp) h] + rw [totient_prime_pow (prime_of_mem_primeDivisors hp) h] #align nat.totient_eq_prod_factorization Nat.totient_eq_prod_factorization /-- Euler's product formula for the totient function. -/ theorem totient_mul_prod_factors (n : ℕ) : - (φ n * ∏ p in n.factors.toFinset, p) = n * ∏ p in n.factors.toFinset, (p - 1) := by + (φ n * ∏ p in n.primeDivisors, p) = n * ∏ p in n.primeDivisors, (p - 1) := by by_cases hn : n = 0; · simp [hn] rw [totient_eq_prod_factorization hn] nth_rw 3 [← factorization_prod_pow_eq_self hn] @@ -303,23 +303,23 @@ theorem totient_mul_prod_factors (n : ℕ) : /-- Euler's product formula for the totient function. -/ theorem totient_eq_div_factors_mul (n : ℕ) : - φ n = (n / ∏ p in n.factors.toFinset, p) * ∏ p in n.factors.toFinset, (p - 1) := by + φ n = (n / ∏ p in n.primeDivisors, p) * ∏ p in n.primeDivisors, (p - 1) := by rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm, - Nat.mul_div_assoc _ (prod_prime_factors_dvd n), mul_comm] - have := prod_pos (fun p => pos_of_mem_factorization (n := n)) - simpa [prod_factorization_eq_prod_factors] using this + Nat.mul_div_assoc _ (prod_primeDivisors_dvd n), mul_comm] + have := prod_pos (fun p => pos_of_mem_primeDivisors (n := n)) + simpa [primeDivisors_eq_factors, prod_factorization_eq_prod_factors] using this #align nat.totient_eq_div_factors_mul Nat.totient_eq_div_factors_mul /-- Euler's product formula for the totient function. -/ theorem totient_eq_mul_prod_factors (n : ℕ) : - (φ n : ℚ) = n * ∏ p in n.factors.toFinset, (1 - (p : ℚ)⁻¹) := by + (φ n : ℚ) = n * ∏ p in n.primeDivisors, (1 - (p : ℚ)⁻¹) := by by_cases hn : n = 0 · simp [hn] have hn' : (n : ℚ) ≠ 0 := by simp [hn] - have hpQ : (∏ p in n.factors.toFinset, (p : ℚ)) ≠ 0 := by + have hpQ : (∏ p in n.primeDivisors, (p : ℚ)) ≠ 0 := by rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors] - exact prod_pos fun p hp => pos_of_mem_factorization hp - simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod, + exact prod_pos fun p hp => pos_of_mem_primeDivisors hp + simp only [totient_eq_div_factors_mul n, prod_primeDivisors_dvd n, cast_mul, cast_prod, cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib] refine' prod_congr rfl fun p hp => _ have hp := pos_of_mem_factors (List.mem_toFinset.mp hp) @@ -340,10 +340,10 @@ theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ simp only [totient_eq_div_factors_mul] rw [shuffle, shuffle] rotate_left - repeat' apply prod_prime_factors_dvd - · simp only [prod_factors_gcd_mul_prod_factors_mul] + repeat' apply prod_primeDivisors_dvd + · simp only [primeDivisors_eq_factors, prod_factors_gcd_mul_prod_factors_mul] rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc] - exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b) + exact mul_dvd_mul (prod_primeDivisors_dvd a) (prod_primeDivisors_dvd b) #align nat.totient_gcd_mul_totient_mul Nat.totient_gcd_mul_totient_mul theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) := by @@ -361,7 +361,7 @@ theorem totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b := by · simp [zero_dvd_iff.1 h] rcases eq_or_ne b 0 with (rfl | hb0) · simp - have hab' : a.factorization.support ⊆ b.factorization.support := by + have hab' : a.primeDivisors ⊆ b.primeDivisors := by intro p simp only [support_factorization, List.mem_toFinset] apply factors_subset_of_dvd h hb0 diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index a5bd4a7e4dfb2..f9c94067906aa 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -203,7 +203,7 @@ theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ} exact fun hd => hp.one_lt.not_le ((mul_le_iff_le_one_left he).mp <| - Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_factorization h) hd) + Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_primeDivisors h) hd) obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ord_proj_dvd _ _ obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h) refine' ⟨g ^ k, _⟩ diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean index bbfa744e9af2c..c373cb4421e05 100644 --- a/Mathlib/GroupTheory/Nilpotent.lean +++ b/Mathlib/GroupTheory/Nilpotent.lean @@ -875,13 +875,13 @@ variable [Fintype G] /-- If a finite group is the direct product of its Sylow groups, it is nilpotent -/ theorem isNilpotent_of_product_of_sylow_group - (e : (∀ p : (Fintype.card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) : + (e : (∀ p : (Fintype.card G).primeDivisors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) : IsNilpotent G := by classical - let ps := (Fintype.card G).factorization.support + let ps := (Fintype.card G).primeDivisors have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by intro p P - haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p)) + haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_primeDivisors (Finset.coe_mem p)) exact P.isPGroup'.isNilpotent exact nilpotent_of_mulEquiv e #align is_nilpotent_of_product_of_sylow_group isNilpotent_of_product_of_sylow_group @@ -894,7 +894,7 @@ theorem isNilpotent_of_finite_tFAE : [IsNilpotent G, NormalizerCondition G, ∀ H : Subgroup G, IsCoatom H → H.Normal, ∀ (p : ℕ) (_hp : Fact p.Prime) (P : Sylow p G), (↑P : Subgroup G).Normal, Nonempty - ((∀ p : (card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] := by + ((∀ p : (card G).primeDivisors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] := by tfae_have 1 → 2 · exact @normalizerCondition_of_isNilpotent _ _ tfae_have 2 → 3 diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean index d89667509b347..e62da5b90cb8c 100644 --- a/Mathlib/GroupTheory/Sylow.lean +++ b/Mathlib/GroupTheory/Sylow.lean @@ -781,14 +781,14 @@ of these Sylow subgroups. -/ noncomputable def directProductOfNormal [Fintype G] (hn : ∀ {p : ℕ} [Fact p.Prime] (P : Sylow p G), (↑P : Subgroup G).Normal) : - (∀ p : (card G).factorization.support, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G := by - set ps := (Fintype.card G).factorization.support + (∀ p : (card G).primeDivisors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G := by + set ps := (Fintype.card G).primeDivisors -- “The” Sylow subgroup for p let P : ∀ p, Sylow p G := default have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne - haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁) - haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂) + haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeDivisors hp₁) + haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeDivisors hp₂) have hne' : p₁ ≠ p₂ := by simpa using hne apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂)) apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup' @@ -798,7 +798,7 @@ noncomputable def directProductOfNormal [Fintype G] · -- here we need to help the elaborator with an explicit instantiation apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _ rintro ⟨p, hp⟩ - haveI hp' := Fact.mk (Nat.prime_of_mem_factorization hp) + haveI hp' := Fact.mk (Nat.prime_of_mem_primeDivisors hp) haveI := subsingleton_of_normal _ (hn (P p)) change (∀ P : Sylow p G, P) ≃* P p exact MulEquiv.piSubsingleton _ _ @@ -810,8 +810,8 @@ noncomputable def directProductOfNormal [Fintype G] · apply Subgroup.injective_noncommPiCoprod_of_independent apply independent_of_coprime_order hcomm rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne - haveI hp₁' := Fact.mk (Nat.prime_of_mem_factorization hp₁) - haveI hp₂' := Fact.mk (Nat.prime_of_mem_factorization hp₂) + haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeDivisors hp₁) + haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeDivisors hp₂) have hne' : p₁ ≠ p₂ := by simpa using hne apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup' show card (∀ p : ps, P p) = card G @@ -819,7 +819,7 @@ noncomputable def directProductOfNormal [Fintype G] card (∀ p : ps, P p) = ∏ p : ps, card (P p) := Fintype.card_pi _ = ∏ p : ps, p.1 ^ (card G).factorization p.1 := by congr 1 with ⟨p, hp⟩ - exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_factorization hp⟩ (P p) + exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeDivisors hp⟩ (P p) _ = ∏ p in ps, p ^ (card G).factorization p := (Finset.prod_finset_coe (fun p => p ^ (card G).factorization p) _) _ = (card G).factorization.prod (· ^ ·) := rfl diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index c1560a04efc68..eab78ad54c333 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -295,7 +295,7 @@ theorem sub_one_norm_isPrimePow (hn : IsPrimePow (n : ℕ)) [IsCyclotomicExtensi obtain ⟨k, hk⟩ : ∃ k, (n : ℕ).factorization (n : ℕ).minFac = k + 1 := exists_eq_succ_of_ne_zero (((n : ℕ).factorization.mem_support_toFun (n : ℕ).minFac).1 <| - factor_iff_mem_factorization.2 <| + factor_iff_mem_primeDivisors.2 <| (mem_factors (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩) simp [hk, sub_one_norm_eq_eval_cyclotomic hζ this hirr] #align is_primitive_root.sub_one_norm_is_prime_pow IsPrimitiveRoot.sub_one_norm_isPrimePow From 4af10f6e48b38fab9e2983fcf8fa276a01983d38 Mon Sep 17 00:00:00 2001 From: Arend Mellendijk Date: Tue, 10 Oct 2023 16:44:42 +0200 Subject: [PATCH 2/4] naming --- Mathlib/Data/Nat/Factorization/Basic.lean | 12 +++++++----- Mathlib/Data/Nat/Squarefree.lean | 2 +- Mathlib/Data/Nat/Totient.lean | 2 +- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 69e5f5bef3583..73765c493056f 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -703,9 +703,9 @@ 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).primeDivisors.prod f * (m * n).primeDivisors.prod f = +@[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 @@ -715,8 +715,10 @@ theorem prod_factors_gcd_mul_prod_factors_mul {β : Type*} [CommMonoid β] (m n congr · apply factors_mul_toFinset <;> assumption · simp only [primeDivisors_eq_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 +#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 diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 908df7f1e3bb5..ea22e2bee3650 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -386,7 +386,7 @@ 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) : +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] diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index be73b87648557..96c6e36a84409 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -341,7 +341,7 @@ theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ rw [shuffle, shuffle] rotate_left repeat' apply prod_primeDivisors_dvd - · simp only [primeDivisors_eq_factors, prod_factors_gcd_mul_prod_factors_mul] + · simp only [prod_primeDivisors_gcd_mul_prod_primeDivisors_mul] rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc] exact mul_dvd_mul (prod_primeDivisors_dvd a) (prod_primeDivisors_dvd b) #align nat.totient_gcd_mul_totient_mul Nat.totient_gcd_mul_totient_mul From 1f45a2cb79acaf952c3e1c716a72a4e54a46569e Mon Sep 17 00:00:00 2001 From: Arend Mellendijk Date: Tue, 10 Oct 2023 17:22:48 +0200 Subject: [PATCH 3/4] add docstring --- Mathlib/Data/Nat/Factorization/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 73765c493056f..8d23017800475 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -122,7 +122,8 @@ 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 -abbrev primeDivisors (n : ℕ) := n.factorization.support +/-- The `Finset` of prime divisors of `n` -/ +abbrev primeDivisors (n : ℕ) : Finset ℕ := n.factorization.support @[simp] theorem primeDivisors_zero : primeDivisors 0 = ∅ := by simp [primeDivisors] From ba4d5d2cb59748b19276d68f93a04a420641c92b Mon Sep 17 00:00:00 2001 From: Arend Mellendijk Date: Thu, 12 Oct 2023 15:31:21 +0200 Subject: [PATCH 4/4] mem_primeDivisors and rename --- Mathlib/Data/Nat/Factorization/Basic.lean | 21 ++++++++++++------- Mathlib/Data/Nat/Factorization/PrimePow.lean | 2 +- .../Cyclotomic/PrimitiveRoots.lean | 2 +- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 8d23017800475..b6c66b487a3a1 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -140,12 +140,19 @@ theorem primeDivisors_eq_factors {n : ℕ} : n.primeDivisors = n.factors.toFinse theorem primeDivisors_eq_factorization {n : ℕ} : n.primeDivisors = n.factorization.support := rfl -theorem factor_iff_mem_primeDivisors {n p : ℕ} : p ∈ n.primeDivisors ↔ p ∈ n.factors := by +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_primeDivisors +#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 + 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_primeDivisors {n p : ℕ} (hp : p ∈ n.primeDivisors) : p.Prime := - prime_of_mem_factors (factor_iff_mem_primeDivisors.mp hp) + mem_primeDivisors.mp hp |>.1 #align nat.prime_of_mem_factorization Nat.prime_of_mem_primeDivisors theorem pos_of_mem_primeDivisors {n p : ℕ} (hp : p ∈ n.primeDivisors) : 0 < p := @@ -153,7 +160,7 @@ theorem pos_of_mem_primeDivisors {n p : ℕ} (hp : p ∈ n.primeDivisors) : 0 < #align nat.pos_of_mem_factorization Nat.pos_of_mem_primeDivisors theorem le_of_mem_primeDivisors {n p : ℕ} (h : p ∈ n.primeDivisors) : p ≤ n := - le_of_mem_factors (factor_iff_mem_primeDivisors.mp h) + 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` -/ @@ -191,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_primeDivisors.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) : @@ -237,7 +244,7 @@ theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : 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_primeDivisors] + simp only [Finset.mem_union, mem_primeDivisors_iff_factor] exact mem_factors_mul ha hb #align nat.factorization_mul_support Nat.primeDivisors_mul @@ -431,7 +438,7 @@ theorem ord_compl_mul (a b p : ℕ) : ord_compl[p] (a * b) = ord_compl[p] a * or 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_primeDivisors h), factor_iff_mem_primeDivisors.mp h] + 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` -/ diff --git a/Mathlib/Data/Nat/Factorization/PrimePow.lean b/Mathlib/Data/Nat/Factorization/PrimePow.lean index 3473c20ab3010..c77b688a0b29f 100644 --- a/Mathlib/Data/Nat/Factorization/PrimePow.lean +++ b/Mathlib/Data/Nat/Factorization/PrimePow.lean @@ -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_primeDivisors, + 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 diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index eab78ad54c333..45f8ed3677109 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -295,7 +295,7 @@ theorem sub_one_norm_isPrimePow (hn : IsPrimePow (n : ℕ)) [IsCyclotomicExtensi obtain ⟨k, hk⟩ : ∃ k, (n : ℕ).factorization (n : ℕ).minFac = k + 1 := exists_eq_succ_of_ne_zero (((n : ℕ).factorization.mem_support_toFun (n : ℕ).minFac).1 <| - factor_iff_mem_primeDivisors.2 <| + mem_primeDivisors_iff_factor.2 <| (mem_factors (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩) simp [hk, sub_one_norm_eq_eval_cyclotomic hζ this hirr] #align is_primitive_root.sub_one_norm_is_prime_pow IsPrimitiveRoot.sub_one_norm_isPrimePow