Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-10 20:24 b9bdc678

View on Github →

feat(*): prove some *.iterate theorems (#2647)

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/calculus/fderiv.lean

Modified src/order/basic.lean

added theorem strict_mono_id

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_mul

modified theorem continuous_linear_map.mul_apply

added theorem continuous_linear_map.mul_def

added theorem continuous_linear_map.smul_right_one_pow

Modified src/topology/basic.lean

added theorem continuous.iterate

added theorem continuous_at.iterate