Commit 2025-02-01 07:23 74bf56fd

View on Github →

chore(Data/ZMod/Basic): split ZMod.valMinAbs off (#21308)

Estimated changes

Modified Archive/Wiedijk100Theorems/FriendshipGraphs.lean

Modified Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

Modified Counterexamples/CliffordAlgebraNotInjective.lean

Modified Counterexamples/HomogeneousPrimeNotPrime.lean

Modified Counterexamples/QuadraticForm.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/ZMod.lean

Modified Mathlib/Data/Nat/Defs.lean

added theorem Nat.le_div_two_iff_mul_two_le

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/ZMod/Basic.lean

deleted theorem Nat.le_div_two_iff_mul_two_le

deleted theorem ZMod.coe_valMinAbs

deleted theorem ZMod.injective_valMinAbs

deleted theorem ZMod.natAbs_valMinAbs_add_le

deleted theorem ZMod.natAbs_valMinAbs_le

deleted theorem ZMod.natAbs_valMinAbs_neg

deleted theorem ZMod.natCast_natAbs_valMinAbs

deleted theorem ZMod.prime_ne_zero

deleted def ZMod.valMinAbs

deleted theorem ZMod.valMinAbs_def_pos

deleted theorem ZMod.valMinAbs_def_zero

deleted theorem ZMod.valMinAbs_eq_zero

deleted theorem ZMod.valMinAbs_mem_Ioc

deleted theorem ZMod.valMinAbs_mul_two_eq_iff

deleted theorem ZMod.valMinAbs_natAbs_eq_min

deleted theorem ZMod.valMinAbs_natCast_eq_self

deleted theorem ZMod.valMinAbs_natCast_of_half_lt

deleted theorem ZMod.valMinAbs_natCast_of_le_half

deleted theorem ZMod.valMinAbs_neg_of_ne_half

deleted theorem ZMod.valMinAbs_nonneg_iff

deleted theorem ZMod.valMinAbs_spec

deleted theorem ZMod.valMinAbs_zero

deleted theorem ZMod.val_eq_ite_valMinAbs

Modified Mathlib/Data/ZMod/Units.lean

Created Mathlib/Data/ZMod/ValMinAbs.lean

added theorem ZMod.coe_valMinAbs

added theorem ZMod.injective_valMinAbs

added theorem ZMod.natAbs_valMinAbs_add_le

added theorem ZMod.natAbs_valMinAbs_le

added theorem ZMod.natAbs_valMinAbs_neg

added theorem ZMod.natCast_natAbs_valMinAbs

added theorem ZMod.prime_ne_zero

added def ZMod.valMinAbs

added theorem ZMod.valMinAbs_def_pos

added theorem ZMod.valMinAbs_def_zero

added theorem ZMod.valMinAbs_eq_zero

added theorem ZMod.valMinAbs_mem_Ioc

added theorem ZMod.valMinAbs_mul_two_eq_iff

added theorem ZMod.valMinAbs_natAbs_eq_min

added theorem ZMod.valMinAbs_natCast_eq_self

added theorem ZMod.valMinAbs_natCast_of_half_lt

added theorem ZMod.valMinAbs_natCast_of_le_half

added theorem ZMod.valMinAbs_neg_of_ne_half

added theorem ZMod.valMinAbs_nonneg_iff

added theorem ZMod.valMinAbs_spec

added theorem ZMod.valMinAbs_zero

added theorem ZMod.val_eq_ite_valMinAbs

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/GroupTheory/Coxeter/Length.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Quaternion.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

Modified Mathlib/RingTheory/Fintype.lean