Commit 2021-06-07 15:40 fb72599b

View on Github →

feat(algebra/periodic): define periodicity (#7572) This PR introduces a general notion of periodicity. It also includes proofs of the "usual" properties of periodic (and antiperiodic) functions.

Estimated changes

Created src/algebra/periodic.lean

added theorem function.antiperiodic.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.div

added theorem function.antiperiodic.div_inv

added theorem function.antiperiodic.eq

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

added theorem function.antiperiodic.neg_eq

added theorem function.antiperiodic.periodic

added theorem function.antiperiodic.sub

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_period

added theorem function.periodic.comp

added theorem function.periodic.comp_add_hom

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_mul

added theorem function.periodic.const_smul'

added theorem function.periodic.const_smul

added theorem function.periodic.div

added theorem function.periodic.div_const

added theorem function.periodic.eq

added theorem function.periodic.gsmul

added theorem function.periodic.gsmul_eq

added theorem function.periodic.int_mul

added theorem function.periodic.int_mul_eq

added theorem function.periodic.mul

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.neg

added theorem function.periodic.neg_eq

added theorem function.periodic.neg_nat_mul

added theorem function.periodic.neg_nsmul

added theorem function.periodic.nsmul

added theorem function.periodic.nsmul_eq

added theorem function.periodic.sub_antiperiod

added theorem function.periodic.sub_antiperiod_eq

added theorem function.periodic.sub_eq

added theorem function.periodic.sub_gsmul_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 def function.periodic

added theorem function.periodic_with_period_zero