bump to nightly-2024-03-02-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Data/Zmod/Quotient.lean

@@ -163,7 +163,7 @@ theorem orbitZPowersEquiv_symm_apply (k : ZMod (minimalPeriod ((· • ·) a) b)
       (⟨a, mem_zpowers a⟩ : zpowers a) ^ (k : ℤ) • ⟨b, mem_orbit_self b⟩ :=
   rfl
 #align mul_action.orbit_zpowers_equiv_symm_apply MulAction.orbitZPowersEquiv_symm_apply
-#align add_action.orbit_zmultiples_equiv_symm_apply AddAction.orbit_zmultiples_equiv_symm_apply
+#align add_action.orbit_zmultiples_equiv_symm_apply AddAction.orbitZMultiplesEquiv_symm_apply
 -/
 
 #print MulAction.orbitZPowersEquiv_symm_apply' /-
@@ -181,7 +181,7 @@ theorem AddAction.orbitZMultiplesEquiv_symm_apply' {α β : Type _} [AddGroup α
     (AddAction.orbitZMultiplesEquiv a b).symm k =
       k • (⟨a, mem_zmultiples a⟩ : zmultiples a) +ᵥ ⟨b, AddAction.mem_orbit_self b⟩ :=
   by
-  rw [AddAction.orbit_zmultiples_equiv_symm_apply, ZMod.coe_int_cast]
+  rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_int_cast]
   exact Subtype.ext (zsmul_vadd_mod_minimal_period _ _ k)
 #align add_action.orbit_zmultiples_equiv_symm_apply' AddAction.orbitZMultiplesEquiv_symm_apply'
 -/

Mathbin/Deprecated/Submonoid.lean

@@ -239,13 +239,13 @@ theorem IsSubmonoid.pow_mem {a : M} (hs : IsSubmonoid s) (h : a ∈ s) : ∀ {n
 #align is_submonoid.pow_mem IsSubmonoid.pow_mem
 -/
 
-#print IsSubmonoid.power_subset /-
+#print IsSubmonoid.powers_subset /-
 /-- The set of natural number powers of an element of a submonoid is a subset of the submonoid. -/
 @[to_additive IsAddSubmonoid.multiples_subset
       "The set of natural number multiples of an element\nof an `add_submonoid` is a subset of the `add_submonoid`."]
-theorem IsSubmonoid.power_subset {a : M} (hs : IsSubmonoid s) (h : a ∈ s) : powers a ⊆ s :=
+theorem IsSubmonoid.powers_subset {a : M} (hs : IsSubmonoid s) (h : a ∈ s) : powers a ⊆ s :=
   fun x ⟨n, hx⟩ => hx ▸ hs.pow_mem h
-#align is_submonoid.power_subset IsSubmonoid.power_subset
+#align is_submonoid.power_subset IsSubmonoid.powers_subset
 #align is_add_submonoid.multiples_subset IsAddSubmonoid.multiples_subset
 -/
 
@@ -379,7 +379,8 @@ theorem closure_mono {s t : Set M} (h : s ⊆ t) : Closure s ⊆ Closure t :=
 theorem closure_singleton {x : M} : Closure ({x} : Set M) = powers x :=
   Set.eq_of_subset_of_subset
       (closure_subset (powers.isSubmonoid x) <| Set.singleton_subset_iff.2 <| powers.self_mem) <|
-    IsSubmonoid.power_subset (closure.isSubmonoid _) <| Set.singleton_subset_iff.1 <| subset_closure
+    IsSubmonoid.powers_subset (closure.isSubmonoid _) <|
+      Set.singleton_subset_iff.1 <| subset_closure
 #align monoid.closure_singleton Monoid.closure_singleton
 #align add_monoid.closure_singleton AddMonoid.closure_singleton
 -/

Mathbin/GroupTheory/OrderOfElement.lean

@@ -1376,27 +1376,27 @@ section Prod
 variable [Monoid α] [Monoid β] {x : α × β} {a : α} {b : β}
 
 #print Prod.orderOf /-
-@[to_additive Prod.add_orderOf]
+@[to_additive Prod.addOrderOf]
 protected theorem Prod.orderOf (x : α × β) : orderOf x = (orderOf x.1).lcm (orderOf x.2) :=
   minimalPeriod_prod_map _ _ _
 #align prod.order_of Prod.orderOf
-#align prod.add_order_of Prod.add_orderOf
+#align prod.add_order_of Prod.addOrderOf
 -/
 
 #print orderOf_fst_dvd_orderOf /-
-@[to_additive add_orderOf_fst_dvd_add_orderOf]
+@[to_additive addOrderOf_fst_dvd_addOrderOf]
 theorem orderOf_fst_dvd_orderOf : orderOf x.1 ∣ orderOf x :=
   minimalPeriod_fst_dvd
 #align order_of_fst_dvd_order_of orderOf_fst_dvd_orderOf
-#align add_order_of_fst_dvd_add_order_of add_orderOf_fst_dvd_add_orderOf
+#align add_order_of_fst_dvd_add_order_of addOrderOf_fst_dvd_addOrderOf
 -/
 
 #print orderOf_snd_dvd_orderOf /-
-@[to_additive add_orderOf_snd_dvd_add_orderOf]
+@[to_additive addOrderOf_snd_dvd_addOrderOf]
 theorem orderOf_snd_dvd_orderOf : orderOf x.2 ∣ orderOf x :=
   minimalPeriod_snd_dvd
 #align order_of_snd_dvd_order_of orderOf_snd_dvd_orderOf
-#align add_order_of_snd_dvd_add_order_of add_orderOf_snd_dvd_add_orderOf
+#align add_order_of_snd_dvd_add_order_of addOrderOf_snd_dvd_addOrderOf
 -/
 
 #print IsOfFinOrder.fst /-

Mathbin/GroupTheory/SpecificGroups/Cyclic.lean

@@ -100,7 +100,7 @@ def IsCyclic.commGroup [hg : Group α] [IsCyclic α] : CommGroup α :=
 variable [Group α]
 
 #print MonoidHom.map_cyclic /-
-@[to_additive MonoidAddHom.map_add_cyclic]
+@[to_additive AddMonoidHom.map_addCyclic]
 theorem MonoidHom.map_cyclic {G : Type _} [Group G] [h : IsCyclic G] (σ : G →* G) :
     ∃ m : ℤ, ∀ g : G, σ g = g ^ m :=
   by
@@ -110,11 +110,11 @@ theorem MonoidHom.map_cyclic {G : Type _} [Group G] [h : IsCyclic G] (σ : G →
   obtain ⟨n, rfl⟩ := hG g
   rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
 #align monoid_hom.map_cyclic MonoidHom.map_cyclic
-#align monoid_add_hom.map_add_cyclic MonoidAddHom.map_add_cyclic
+#align monoid_add_hom.map_add_cyclic AddMonoidHom.map_addCyclic
 -/
 
 #print isCyclic_of_orderOf_eq_card /-
-@[to_additive isAddCyclic_of_orderOf_eq_card]
+@[to_additive isAddCyclic_of_addOrderOf_eq_card]
 theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) :
     IsCyclic α := by
   classical
@@ -123,7 +123,7 @@ theorem isCyclic_of_orderOf_eq_card [Fintype α] (x : α) (hx : orderOf x = Fint
   rw [← Fintype.card_congr (Equiv.Set.univ α), Fintype.card_zpowers] at hx 
   exact Set.eq_of_subset_of_card_le (Set.subset_univ _) (ge_of_eq hx)
 #align is_cyclic_of_order_of_eq_card isCyclic_of_orderOf_eq_card
-#align is_add_cyclic_of_order_of_eq_card isAddCyclic_of_orderOf_eq_card
+#align is_add_cyclic_of_order_of_eq_card isAddCyclic_of_addOrderOf_eq_card
 -/
 
 #print isCyclic_of_prime_card /-
@@ -259,7 +259,7 @@ open scoped Classical
 
 /- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:133:4: warning: unsupported: rw with cfg: { occs := occurrences.pos[occurrences.pos] «expr[ ,]»([2, 3]) } -/
 #print IsCyclic.card_pow_eq_one_le /-
-@[to_additive IsAddCyclic.card_pow_eq_one_le]
+@[to_additive IsAddCyclic.card_nsmul_eq_zero_le]
 theorem IsCyclic.card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :
     (univ.filterₓ fun a : α => a ^ n = 1).card ≤ n :=
   let ⟨g, hg⟩ := IsCyclic.exists_generator α
@@ -291,7 +291,7 @@ theorem IsCyclic.card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α]
         Nat.mul_div_cancel _ hm0]
       exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)
 #align is_cyclic.card_pow_eq_one_le IsCyclic.card_pow_eq_one_le
-#align is_add_cyclic.card_pow_eq_one_le IsAddCyclic.card_pow_eq_one_le
+#align is_add_cyclic.card_pow_eq_one_le IsAddCyclic.card_nsmul_eq_zero_le
 -/
 
 end Classical
@@ -451,16 +451,14 @@ theorem IsCyclic.card_orderOf_eq_totient [IsCyclic α] [Fintype α] {d : ℕ}
 #align is_cyclic.card_order_of_eq_totient IsCyclic.card_orderOf_eq_totient
 -/
 
-#print IsAddCyclic.card_orderOf_eq_totient /-
-theorem IsAddCyclic.card_orderOf_eq_totient {α} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ}
+theorem IsAddCyclic.card_order_of_eq_totient {α} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ}
     (hd : d ∣ Fintype.card α) : (univ.filterₓ fun a : α => addOrderOf a = d).card = totient d :=
   by
   obtain ⟨g, hg⟩ := id ‹IsAddCyclic α›
   exact @IsCyclic.card_orderOf_eq_totient (Multiplicative α) _ ⟨⟨g, hg⟩⟩ _ _ hd
-#align is_add_cyclic.card_order_of_eq_totient IsAddCyclic.card_orderOf_eq_totient
--/
+#align is_add_cyclic.card_order_of_eq_totient IsAddCyclic.card_order_of_eq_totient
 
-attribute [to_additive IsCyclic.card_orderOf_eq_totient] IsAddCyclic.card_orderOf_eq_totient
+attribute [to_additive IsCyclic.card_orderOf_eq_totient] IsAddCyclic.card_order_of_eq_totient
 
 #print isSimpleGroup_of_prime_card /-
 /-- A finite group of prime order is simple. -/
@@ -494,7 +492,7 @@ variable {G : Type _} {H : Type _} [Group G] [Group H]
 #print commutative_of_cyclic_center_quotient /-
 /-- A group is commutative if the quotient by the center is cyclic.
   Also see `comm_group_of_cycle_center_quotient` for the `comm_group` instance. -/
-@[to_additive commutative_of_add_cyclic_center_quotient
+@[to_additive commutative_of_addCyclic_center_quotient
       "A group is commutative if the quotient by\n  the center is cyclic. Also see `add_comm_group_of_cycle_center_quotient`\n  for the `add_comm_group` instance."]
 theorem commutative_of_cyclic_center_quotient [IsCyclic H] (f : G →* H) (hf : f.ker ≤ center G)
     (a b : G) : a * b = b * a :=
@@ -514,7 +512,7 @@ theorem commutative_of_cyclic_center_quotient [IsCyclic H] (f : G →* H) (hf :
     _ = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) := by rw [mem_center_iff.1 hb]
     _ = b * a := by group
 #align commutative_of_cyclic_center_quotient commutative_of_cyclic_center_quotient
-#align commutative_of_add_cyclic_center_quotient commutative_of_add_cyclic_center_quotient
+#align commutative_of_add_cyclic_center_quotient commutative_of_addCyclic_center_quotient
 -/
 
 #print commGroupOfCycleCenterQuotient /-

Mathbin/Topology/Algebra/InfiniteSum/Basic.lean

@@ -487,12 +487,10 @@ theorem Summable.compl_add {s : Set β} (hs : Summable (f ∘ coe : sᶜ → α)
 #align summable.compl_add Summable.compl_add
 -/
 
-#print Summable.even_add_odd /-
 theorem Summable.even_add_odd {f : ℕ → α} (he : Summable fun k => f (2 * k))
     (ho : Summable fun k => f (2 * k + 1)) : Summable f :=
   (he.HasSum.even_add_odd ho.HasSum).Summable
 #align summable.even_add_odd Summable.even_add_odd
--/
 
 #print HasSum.sigma /-
 theorem HasSum.sigma [RegularSpace α] {γ : β → Type _} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α}

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "rev": "c7394bfb27f466a0cd35d0003d4dba824b94b3d4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "inputRev": "c7394bfb27f466a0cd35d0003d4dba824b94b3d4",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "2ce78e64d42077972ea92915361746978c8cfbff",
+   "rev": "465f4e273c40e81bb92296ab5d2bb0332a0aa862",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2ce78e64d42077972ea92915361746978c8cfbff",
+   "inputRev": "465f4e273c40e81bb92296ab5d2bb0332a0aa862",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2024-03-01-08"
+def tag : String := "nightly-2024-03-02-08"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2ce78e64d42077972ea92915361746978c8cfbff"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"465f4e273c40e81bb92296ab5d2bb0332a0aa862"
 
 @[default_target]
 lean_lib Mathbin where