Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-31 13:11 b64b1f88

View on Github →

feat(algebra/periodic): generalize some lemmas (#18334)

Drop some commutativity assumptions.
Golf some proofs.
Add protected here and there for future compatibility with Lean 4.

Estimated changes

Modified src/algebra/periodic.lean

deleted theorem function.antiperiodic.add

deleted theorem function.antiperiodic.div

deleted theorem function.antiperiodic.div_inv

deleted theorem function.antiperiodic.eq

deleted theorem function.antiperiodic.funext'

deleted theorem function.antiperiodic.funext

modified theorem function.antiperiodic.int_mul_eq_of_eq_zero

deleted theorem function.antiperiodic.mul

modified theorem function.antiperiodic.nat_mul_eq_of_eq_zero

deleted theorem function.antiperiodic.neg

deleted theorem function.antiperiodic.periodic

deleted theorem function.antiperiodic.smul

deleted theorem function.antiperiodic.sub

modified theorem function.antiperiodic.sub_eq'

modified theorem function.periodic.add_period

deleted theorem function.periodic.comp

modified theorem function.periodic.const_inv_mul

deleted theorem function.periodic.const_mul

deleted theorem function.periodic.const_smul

deleted theorem function.periodic.div

modified theorem function.periodic.div_const

deleted theorem function.periodic.eq

deleted theorem function.periodic.funext

deleted theorem function.periodic.int_mul

modified theorem function.periodic.int_mul_eq

modified theorem function.periodic.int_mul_sub_eq

deleted theorem function.periodic.mul

modified theorem function.periodic.mul_const

modified theorem function.periodic.mul_const_inv

modified theorem function.periodic.nat_mul

modified theorem function.periodic.nat_mul_eq

modified theorem function.periodic.nat_mul_sub_eq

deleted theorem function.periodic.neg

deleted theorem function.periodic.neg_eq

modified theorem function.periodic.neg_nat_mul

modified theorem function.periodic.neg_nsmul

modified theorem function.periodic.nsmul

deleted theorem function.periodic.nsmul_eq

modified theorem function.periodic.nsmul_sub_eq

deleted theorem function.periodic.smul

modified theorem function.periodic.sub_antiperiod

modified theorem function.periodic.sub_antiperiod_eq

modified theorem function.periodic.sub_eq'

modified theorem function.periodic.sub_eq

modified theorem function.periodic.sub_int_mul_eq

modified theorem function.periodic.sub_nat_mul_eq

modified theorem function.periodic.sub_nsmul_eq

modified theorem function.periodic.sub_period

modified theorem function.periodic.sub_zsmul_eq

deleted theorem function.periodic.zsmul

modified theorem function.periodic.zsmul_eq

modified theorem function.periodic.zsmul_sub_eq

modified theorem list.periodic_prod