chore(Periodic): don't import Field

Mathlib.lean

@@ -244,12 +244,15 @@ import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Field.Equiv
 import Mathlib.Algebra.Field.IsField
 import Mathlib.Algebra.Field.MinimalAxioms
+import Mathlib.Algebra.Field.NegOnePow
 import Mathlib.Algebra.Field.Opposite
+import Mathlib.Algebra.Field.Periodic
 import Mathlib.Algebra.Field.Power
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Field.Subfield.Basic
 import Mathlib.Algebra.Field.Subfield.Defs
 import Mathlib.Algebra.Field.ULift
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.Free
 import Mathlib.Algebra.FreeAlgebra
 import Mathlib.Algebra.FreeAlgebra.Cardinality
@@ -849,7 +852,6 @@ import Mathlib.Algebra.Order.ToIntervalMod
 import Mathlib.Algebra.Order.UpperLower
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Algebra.PEmptyInstances
-import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.Pointwise.Stabilizer
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Basic
@@ -955,6 +957,7 @@ import Mathlib.Algebra.Ring.NonZeroDivisors
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Algebra.Ring.PUnit
 import Mathlib.Algebra.Ring.Parity
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Algebra.Ring.Pi
 import Mathlib.Algebra.Ring.Pointwise.Finset
 import Mathlib.Algebra.Ring.Pointwise.Set

Mathlib/Algebra/Field/NegOnePow.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou, Johan Commelin
+-/
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Ring.NegOnePow
+import Mathlib.Tactic.NormNum
+
+/-! # Integer powers of `-1` in a field -/
+
+namespace Int
+
+lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n := by
+  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
+  · simp [zpow_mul, zpow_ofNat]
+  · rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]
+    simp
+
+@[deprecated (since := "2024-10-20")] alias coe_negOnePow := cast_negOnePow
+
+end Int

Mathlib/Algebra/Field/Periodic.lean

@@ -0,0 +1,164 @@
+/-
+Copyright (c) 2021 Benjamin Davidson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Davidson
+-/
+import Mathlib.Algebra.Field.Opposite
+import Mathlib.Algebra.Module.Opposite
+import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Ring.Periodic
+
+/-!
+# Periodic functions
+
+This file proves facts about periodic and antiperiodic functions from and to a field.
+
+## Main definitions
+
+* `Function.Periodic`: A function `f` is *periodic* if `∀ x, f (x + c) = f x`.
+  `f` is referred to as periodic with period `c` or `c`-periodic.
+
+* `Function.Antiperiodic`: A function `f` is *antiperiodic* if `∀ x, f (x + c) = -f x`.
+  `f` is referred to as antiperiodic with antiperiod `c` or `c`-antiperiodic.
+
+Note that any `c`-antiperiodic function will necessarily also be `2 • c`-periodic.
+
+## Tags
+
+period, periodic, periodicity, antiperiodic
+-/
+
+assert_not_exists TwoSidedIdeal
+
+variable {α β γ : Type*} {f g : α → β} {c c₁ c₂ x : α}
+
+open Set
+
+namespace Function
+
+/-! ### Periodicity -/
+
+protected theorem Periodic.const_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
+    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
+  by_cases ha : a = 0
+  · simp only [ha, zero_smul]
+  · simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
+
+protected theorem Periodic.const_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (a * x)) (a⁻¹ * c) :=
+  Periodic.const_smul₀ h a
+
+theorem Periodic.const_inv_smul₀ [AddCommMonoid α] [DivisionSemiring γ] [Module γ α]
+    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a⁻¹ • x)) (a • c) := by
+  simpa only [inv_inv] using h.const_smul₀ a⁻¹
+
+theorem Periodic.const_inv_mul [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (a⁻¹ * x)) (a * c) :=
+  h.const_inv_smul₀ a
+
+theorem Periodic.mul_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a)) (c * a⁻¹) :=
+  h.const_smul₀ (MulOpposite.op a)
+
+theorem Periodic.mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a)) (c / a) := by simpa only [div_eq_mul_inv] using h.mul_const a
+
+theorem Periodic.mul_const_inv [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x * a⁻¹)) (c * a) :=
+  h.const_inv_smul₀ (MulOpposite.op a)
+
+theorem Periodic.div_const [DivisionSemiring α] (h : Periodic f c) (a : α) :
+    Periodic (fun x => f (x / a)) (c * a) := by simpa only [div_eq_mul_inv] using h.mul_const_inv a
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ico 0 c` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ico₀ [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
+  ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ico a (a + c)` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ico [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
+  ⟨x + n • c, H, (h.zsmul n x).symm⟩
+
+/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
+  `y ∈ Ioc a (a + c)` such that `f x = f y`. -/
+theorem Periodic.exists_mem_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y :=
+  let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
+  ⟨x + n • c, H, (h.zsmul n x).symm⟩
+
+theorem Periodic.image_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <| range_subset_iff.2 fun x =>
+    let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
+    ⟨y, hy, hyx.symm⟩
+
+theorem Periodic.image_Icc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_subset _ Ioc_subset_Icc_self
+
+theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by
+  cases hc.lt_or_lt with
+  | inl hc =>
+    rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
+      add_neg_cancel_right]
+  | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
+
+/-! ### Antiperiodicity -/
+
+theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (x + n * c) = (-1) ^ n * f x := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.add_nsmul_eq n
+
+theorem Antiperiodic.sub_nat_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (x - n * c) = (-1) ^ n * f x := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.sub_nsmul_eq n
+
+theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
+    f (n * c - x) = (-1) ^ n * f (-x) := by
+  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
+    Int.cast_one] using h.nsmul_sub_eq n
+
+theorem Antiperiodic.const_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) :=
+  fun x => by simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)
+
+theorem Antiperiodic.const_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (a * x)) (a⁻¹ * c) :=
+  h.const_smul₀ ha
+
+theorem Antiperiodic.const_inv_smul₀ [AddCommMonoid α] [Neg β] [DivisionSemiring γ] [Module γ α]
+    (h : Antiperiodic f c) {a : γ} (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ • x)) (a • c) := by
+  simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)
+
+theorem Antiperiodic.const_inv_mul [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (a⁻¹ * x)) (a * c) :=
+  h.const_inv_smul₀ ha
+
+theorem Antiperiodic.mul_const [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c * a⁻¹) :=
+  h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
+
+theorem Antiperiodic.mul_const' [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a)) (c / a) := by
+  simpa only [div_eq_mul_inv] using h.mul_const ha
+
+theorem Antiperiodic.mul_const_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x * a⁻¹)) (c * a) :=
+  h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha
+
+theorem Antiperiodic.div_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
+    (ha : a ≠ 0) : Antiperiodic (fun x => f (x / a)) (c * a) := by
+  simpa only [div_eq_mul_inv] using h.mul_const_inv ha
+
+end Function
+
+theorem Int.fract_periodic (α) [LinearOrderedRing α] [FloorRing α] :
+    Function.Periodic Int.fract (1 : α) := fun a => mod_cast Int.fract_add_int a 1

Mathlib/Algebra/Field/ZMod.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Mathlib.Algebra.Field.Basic
+import Mathlib.Data.ZMod.Basic
+
+/-!
+# `ZMod p` is a field
+-/
+
+namespace ZMod
+variable (p : ℕ) [hp : Fact p.Prime]
+
+private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 := by
+  obtain ⟨k, rfl⟩ := natCast_zmod_surjective a
+  apply coe_mul_inv_eq_one
+  apply Nat.Coprime.symm
+  rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
+
+/-- Field structure on `ZMod p` if `p` is prime. -/
+instance : Field (ZMod p) where
+  mul_inv_cancel := mul_inv_cancel_aux p
+  inv_zero := inv_zero p
+  nnqsmul := _
+  nnqsmul_def := fun _ _ => rfl
+  qsmul := _
+  qsmul_def := fun _ _ => rfl
+
+/-- `ZMod p` is an integral domain when `p` is prime. -/
+instance : IsDomain (ZMod p) := by
+  -- We need `cases p` here in order to resolve which `CommRing` instance is being used.
+  cases p
+  · exact (Nat.not_prime_zero hp.out).elim
+  exact @Field.isDomain (ZMod _) (inferInstanceAs (Field (ZMod _)))
+
+end ZMod

Mathlib/Algebra/Homology/ComplexShapeSigns.lean

@@ -24,7 +24,7 @@ satisfying certain properties (see `ComplexShape.TensorSigns`).
 
 -/
 
-assert_not_exists TwoSidedIdeal
+assert_not_exists Field TwoSidedIdeal
 
 variable {I₁ I₂ I₃ I₁₂ I₂₃ J : Type*}
   (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃)

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
 import Mathlib.Algebra.ModEq
-import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Order.Archimedean.Basic
-import Mathlib.Algebra.Periodic
+import Mathlib.Algebra.Ring.Periodic
 import Mathlib.Data.Int.SuccPred
 import Mathlib.Order.Circular
-import Mathlib.Data.List.TFAE
-import Mathlib.Data.Set.Lattice
 
 /-!
 # Reducing to an interval modulo its length

Mathlib/Algebra/Ring/NegOnePow.lean

@@ -6,7 +6,6 @@ Authors: Joël Riou, Johan Commelin
 import Mathlib.Algebra.Ring.Int.Parity
 import Mathlib.Algebra.Ring.Int.Units
 import Mathlib.Data.ZMod.IntUnitsPower
-import Mathlib.Tactic.NormNum
 
 /-!
 # Integer powers of (-1)
@@ -18,6 +17,7 @@ Johan Commelin to the Liquid Tensor Experiment.
 
 -/
 
+assert_not_exists Field
 assert_not_exists TwoSidedIdeal
 
 namespace Int
@@ -105,14 +105,6 @@ lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
 lemma negOnePow_mul_self (n : ℤ) : (n * n).negOnePow = n.negOnePow := by
   simpa [mul_sub, negOnePow_eq_iff] using n.even_mul_pred_self
 
-lemma cast_negOnePow (K : Type*) (n : ℤ) [Field K] : n.negOnePow = (-1 : K) ^ n := by
-  rcases even_or_odd' n with ⟨k, rfl | rfl⟩
-  · simp [zpow_mul, zpow_ofNat]
-  · rw [zpow_add_one₀ (by norm_num), zpow_mul, zpow_ofNat]
-    simp
-
-@[deprecated (since := "2024-10-20")] alias coe_negOnePow := cast_negOnePow
-
 lemma cast_negOnePow_natCast (R : Type*) [Ring R] (n : ℕ) : negOnePow n = (-1 : R) ^ n := by
   obtain ⟨k, rfl | rfl⟩ := Nat.even_or_odd' n <;> simp [pow_succ, pow_mul]