Commit 2025-02-14 13:43 7e65b685

View on Github →

chore(Periodic): don't import Field (#20552)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Field/Periodic.lean

added theorem Function.Antiperiodic.add_nat_mul_eq

added theorem Function.Antiperiodic.const_inv_mul

added theorem Function.Antiperiodic.const_inv_smul₀

added theorem Function.Antiperiodic.const_mul

added theorem Function.Antiperiodic.const_smul₀

added theorem Function.Antiperiodic.div_inv

added theorem Function.Antiperiodic.mul_const'

added theorem Function.Antiperiodic.mul_const

added theorem Function.Antiperiodic.mul_const_inv

added theorem Function.Antiperiodic.nat_mul_sub_eq

added theorem Function.Antiperiodic.sub_nat_mul_eq

added theorem Function.Periodic.const_inv_mul

added theorem Function.Periodic.const_inv_smul₀

added theorem Function.Periodic.div_const

added theorem Function.Periodic.exists_mem_Ico

added theorem Function.Periodic.exists_mem_Ico₀

added theorem Function.Periodic.exists_mem_Ioc

added theorem Function.Periodic.image_Icc

added theorem Function.Periodic.image_Ioc

added theorem Function.Periodic.image_uIcc

added theorem Function.Periodic.mul_const'

added theorem Function.Periodic.mul_const

added theorem Function.Periodic.mul_const_inv

added theorem Int.fract_periodic

Modified Mathlib/Algebra/Order/ToIntervalMod.lean

Renamed Mathlib/Algebra/Periodic.lean to Mathlib/Algebra/Ring/Periodic.lean

deleted theorem Function.Antiperiodic.add_nat_mul_eq

deleted theorem Function.Antiperiodic.const_inv_mul

deleted theorem Function.Antiperiodic.const_inv_smul₀

deleted theorem Function.Antiperiodic.const_mul

deleted theorem Function.Antiperiodic.const_smul₀

deleted theorem Function.Antiperiodic.div_inv

deleted theorem Function.Antiperiodic.mul_const'

deleted theorem Function.Antiperiodic.mul_const

deleted theorem Function.Antiperiodic.mul_const_inv

deleted theorem Function.Antiperiodic.nat_mul_sub_eq

deleted theorem Function.Antiperiodic.sub_nat_mul_eq

deleted theorem Function.Periodic.const_inv_mul

deleted theorem Function.Periodic.const_inv_smul₀

deleted theorem Function.Periodic.div_const

deleted theorem Function.Periodic.exists_mem_Ico

deleted theorem Function.Periodic.exists_mem_Ico₀

deleted theorem Function.Periodic.exists_mem_Ioc

deleted theorem Function.Periodic.image_Icc

deleted theorem Function.Periodic.image_Ioc

deleted theorem Function.Periodic.image_uIcc

deleted theorem Function.Periodic.mul_const'

deleted theorem Function.Periodic.mul_const

deleted theorem Function.Periodic.mul_const_inv

deleted theorem Int.fract_periodic

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/Data/Nat/Periodic.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/NumberTheory/FermatPsp.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/Topology/ContinuousMap/Periodic.lean

Modified Mathlib/Topology/Instances/Real/Lemmas.lean

Modified Mathlib/Topology/Instances/ZMultiples.lean