Theoremsperiodic_prod, periodic_sum, add, add_const, add_int_mul_eq, add_nsmul_eq, add_zsmul_eq, const_add, const_inv_smul, const_smul, const_sub, div, eq, even_nsmul_periodic, even_zsmul_periodic, funext, funext', int_even_mul_periodic, int_mul_eq_of_eq_zero, int_mul_sub_eq, int_odd_mul_antiperiodic, mul, nat_even_mul_periodic, nat_mul_eq_of_eq_zero, nat_odd_mul_antiperiodic, neg, neg_eq, nsmul_sub_eq, odd_nsmul_antiperiodic, odd_zsmul_antiperiodic, periodic, periodic_two_mul, smul, sub, sub_const, sub_eq, sub_eq', sub_int_mul_eq, sub_nsmul_eq, sub_zsmul_eq, zsmul_sub_eq, periodic_iterate, add, add_antiperiod, add_antiperiod_eq, add_const, add_period, comp, comp_addHom, const_add, const_inv_smul, const_smul, const_sub, div, eq, funext, int_mul, int_mul_eq, int_mul_sub_eq, isPeriodicPt, lift_coe, map_vadd_multiples, map_vadd_zmultiples, mul, nat_mul, nat_mul_eq, nat_mul_sub_eq, neg, neg_eq, neg_nat_mul, neg_nsmul, not_injective, nsmul, nsmul_eq, nsmul_sub_eq, smul, sub, sub_antiperiod, sub_antiperiod_eq, sub_const, sub_eq, sub_eq', sub_int_mul_eq, sub_nat_mul_eq, sub_nsmul_eq, sub_period, sub_zsmul_eq, vadd, zsmul, zsmul_eq, zsmul_sub_eq, periodic_iterate_iff, periodic_with_period_zero, periodic_prod, periodic_sum, periodic_prod, periodic_sum | 97 |