Commit 2023-02-06 02:05 f06fc319

View on Github →

feat: port Algebra.Periodic (#1963)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Periodic.lean

added theorem Finset.periodic_prod

added theorem Function.Antiperiodic.add

added theorem Function.Antiperiodic.add_const

added theorem Function.Antiperiodic.const_add

added theorem Function.Antiperiodic.const_inv_mul

added theorem Function.Antiperiodic.const_inv_smul

added theorem Function.Antiperiodic.const_inv_smul₀

added theorem Function.Antiperiodic.const_mul

added theorem Function.Antiperiodic.const_smul

added theorem Function.Antiperiodic.const_smul₀

added theorem Function.Antiperiodic.const_sub

added theorem Function.Antiperiodic.div

added theorem Function.Antiperiodic.div_inv

added theorem Function.Antiperiodic.int_even_mul_periodic

added theorem Function.Antiperiodic.int_mul_eq_of_eq_zero

added theorem Function.Antiperiodic.int_odd_mul_antiperiodic

added theorem Function.Antiperiodic.mul

added theorem Function.Antiperiodic.mul_const'

added theorem Function.Antiperiodic.mul_const

added theorem Function.Antiperiodic.mul_const_inv

added theorem Function.Antiperiodic.nat_even_mul_periodic

added theorem Function.Antiperiodic.nat_mul_eq_of_eq_zero

added theorem Function.Antiperiodic.nat_odd_mul_antiperiodic

added theorem Function.Antiperiodic.neg_eq

added theorem Function.Antiperiodic.smul

added theorem Function.Antiperiodic.sub

added theorem Function.Antiperiodic.sub_const

added theorem Function.Antiperiodic.sub_eq'

added theorem Function.Antiperiodic.sub_eq

added def Function.Antiperiodic

added theorem Function.Periodic.add_antiperiod

added theorem Function.Periodic.add_antiperiod_eq

added theorem Function.Periodic.add_const

added theorem Function.Periodic.add_period

added theorem Function.Periodic.comp_addHom

added theorem Function.Periodic.const_add

added theorem Function.Periodic.const_inv_mul

added theorem Function.Periodic.const_inv_smul

added theorem Function.Periodic.const_inv_smul₀

added theorem Function.Periodic.const_sub

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_Ioc

added theorem Function.Periodic.int_mul_eq

added theorem Function.Periodic.int_mul_sub_eq

added def Function.Periodic.lift

added theorem Function.Periodic.lift_coe

added theorem Function.Periodic.map_vadd_multiples

added theorem Function.Periodic.map_vadd_zmultiples

added theorem Function.Periodic.mul_const'

added theorem Function.Periodic.mul_const

added theorem Function.Periodic.mul_const_inv

added theorem Function.Periodic.nat_mul

added theorem Function.Periodic.nat_mul_eq

added theorem Function.Periodic.nat_mul_sub_eq

added theorem Function.Periodic.neg_nat_mul

added theorem Function.Periodic.neg_nsmul

added theorem Function.Periodic.nsmul

added theorem Function.Periodic.nsmul_sub_eq

added theorem Function.Periodic.sub_antiperiod

added theorem Function.Periodic.sub_antiperiod_eq

added theorem Function.Periodic.sub_const

added theorem Function.Periodic.sub_eq'

added theorem Function.Periodic.sub_eq

added theorem Function.Periodic.sub_int_mul_eq

added theorem Function.Periodic.sub_nat_mul_eq

added theorem Function.Periodic.sub_nsmul_eq

added theorem Function.Periodic.sub_period

added theorem Function.Periodic.sub_zsmul_eq

added theorem Function.Periodic.zsmul_eq

added theorem Function.Periodic.zsmul_sub_eq

added def Function.Periodic

added theorem Function.periodic_with_period_zero

added theorem Int.fract_periodic

added theorem List.periodic_prod

added theorem Multiset.periodic_prod