Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-15 19:12 7803884e

View on Github →

feat(data/pi): Composition of addition/subtraction/... of functions (#10305)

Estimated changes

Modified src/algebra/group/pi.lean

deleted theorem pi.comp_one

deleted theorem pi.const_one

deleted theorem pi.one_comp

Modified src/data/pi.lean

added theorem pi.comp_one

added theorem pi.const_div

added theorem pi.const_inv

added theorem pi.const_mul

added theorem pi.const_one

added theorem pi.div_comp

added theorem pi.inv_comp

added theorem pi.mul_comp

added theorem pi.one_comp