From 3092e6a815dbdaeacc81b1c7dd5540d81cfdfc4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 1 Feb 2025 08:41:33 +0000 Subject: [PATCH] chore(Data/ZMod/Basic): don't import `Field` --- Mathlib.lean | 2 + Mathlib/Algebra/Field/NegOnePow.lean | 22 +++++++++++ Mathlib/Algebra/Field/ZMod.lean | 38 +++++++++++++++++++ Mathlib/Algebra/Ring/NegOnePow.lean | 10 +---- .../SpecialFunctions/Trigonometric/Basic.lean | 2 +- Mathlib/Data/ZMod/Basic.lean | 27 +------------ Mathlib/FieldTheory/Finite/Basic.lean | 1 + .../IsAlgClosed/Classification.lean | 1 + Mathlib/NumberTheory/LucasPrimality.lean | 1 + Mathlib/NumberTheory/Padics/RingHoms.lean | 3 +- Mathlib/RingTheory/Polynomial/Dickson.lean | 1 + MathlibTest/instance_diamonds.lean | 1 + 12 files changed, 72 insertions(+), 37 deletions(-) create mode 100644 Mathlib/Algebra/Field/NegOnePow.lean create mode 100644 Mathlib/Algebra/Field/ZMod.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2b4b3f356c390..6ac5f56d7b3ce 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -240,12 +240,14 @@ 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.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 diff --git a/Mathlib/Algebra/Field/NegOnePow.lean b/Mathlib/Algebra/Field/NegOnePow.lean new file mode 100644 index 0000000000000..09830004cd053 --- /dev/null +++ b/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 diff --git a/Mathlib/Algebra/Field/ZMod.lean b/Mathlib/Algebra/Field/ZMod.lean new file mode 100644 index 0000000000000..7b0a67667b68b --- /dev/null +++ b/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 diff --git a/Mathlib/Algebra/Ring/NegOnePow.lean b/Mathlib/Algebra/Ring/NegOnePow.lean index 62d61d99068ed..194d23e68cc1a 100644 --- a/Mathlib/Algebra/Ring/NegOnePow.lean +++ b/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] diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean index e2816cc24eaff..a45c9c280dc27 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean @@ -3,9 +3,9 @@ Copyright (c) 2018 Chris Hughes. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson -/ +import Mathlib.Algebra.Field.NegOnePow import Mathlib.Algebra.Periodic import Mathlib.Algebra.QuadraticDiscriminant -import Mathlib.Algebra.Ring.NegOnePow import Mathlib.Analysis.SpecialFunctions.Exp import Mathlib.Tactic.Positivity.Core diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 59afdd1965ae0..890c9d1e9851f 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ import Mathlib.Algebra.CharP.Basic -import Mathlib.Algebra.Field.Basic import Mathlib.Algebra.Module.End import Mathlib.Algebra.Ring.Prod import Mathlib.Data.Fintype.Units @@ -31,7 +30,7 @@ This is a ring hom if the ring has characteristic dividing `n` -/ -assert_not_exists Submodule TwoSidedIdeal +assert_not_exists Field Submodule TwoSidedIdeal open Function ZMod @@ -1051,30 +1050,6 @@ theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) ( refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm) rw [← mul_two]; apply Nat.div_mul_le_self -variable (p : ℕ) [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 instField : 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 (p : ℕ) [hp : Fact p.Prime] : 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 theorem RingHom.ext_zmod {n : ℕ} {R : Type*} [Semiring R] (f g : ZMod n →+* R) : f = g := by diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean index caa9cfdf653ab..067d08dc8698d 100644 --- a/Mathlib/FieldTheory/Finite/Basic.lean +++ b/Mathlib/FieldTheory/Finite/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes, Joey van Langen, Casper Putz -/ import Mathlib.Algebra.CharP.Reduced +import Mathlib.Algebra.Field.ZMod import Mathlib.Data.ZMod.ValMinAbs import Mathlib.FieldTheory.Separable import Mathlib.RingTheory.IntegralDomain diff --git a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean index 4ca1dd6b4fbde..04457a24183d8 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Classification.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Classification.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ import Mathlib.Algebra.Algebra.ZMod +import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.MvPolynomial.Cardinal import Mathlib.Algebra.Polynomial.Cardinal import Mathlib.FieldTheory.IsAlgClosed.Basic diff --git a/Mathlib/NumberTheory/LucasPrimality.lean b/Mathlib/NumberTheory/LucasPrimality.lean index 34deef6e5fc10..39e0f93a7b61b 100644 --- a/Mathlib/NumberTheory/LucasPrimality.lean +++ b/Mathlib/NumberTheory/LucasPrimality.lean @@ -3,6 +3,7 @@ Copyright (c) 2020 Bolton Bailey. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bolton Bailey -/ +import Mathlib.Algebra.Field.ZMod import Mathlib.RingTheory.IntegralDomain /-! diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean index a4bc7e4bf2fd8..bb16e4b29ac1e 100644 --- a/Mathlib/NumberTheory/Padics/RingHoms.lean +++ b/Mathlib/NumberTheory/Padics/RingHoms.lean @@ -3,8 +3,9 @@ Copyright (c) 2020 Johan Commelin, Robert Y. Lewis. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Robert Y. Lewis -/ -import Mathlib.RingTheory.LocalRing.ResidueField.Defs +import Mathlib.Algebra.Field.ZMod import Mathlib.NumberTheory.Padics.PadicIntegers +import Mathlib.RingTheory.LocalRing.ResidueField.Defs import Mathlib.RingTheory.ZMod /-! diff --git a/Mathlib/RingTheory/Polynomial/Dickson.lean b/Mathlib/RingTheory/Polynomial/Dickson.lean index d1a85a4548180..aee0c850d5b64 100644 --- a/Mathlib/RingTheory/Polynomial/Dickson.lean +++ b/Mathlib/RingTheory/Polynomial/Dickson.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.CharP.Algebra import Mathlib.Algebra.CharP.Invertible import Mathlib.Algebra.CharP.Lemmas import Mathlib.Algebra.EuclideanDomain.Field +import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.Polynomial.Roots import Mathlib.RingTheory.Polynomial.Chebyshev diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean index 02932d2f6192b..1dffa9c372c1c 100644 --- a/MathlibTest/instance_diamonds.lean +++ b/MathlibTest/instance_diamonds.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Eric Wieser -/ import Mathlib.Algebra.EuclideanDomain.Field +import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.GroupWithZero.Action.Prod import Mathlib.Algebra.GroupWithZero.Action.Units import Mathlib.Algebra.Module.Pi