Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-24 14:15 7a718662

View on Github →

chore(topology/algebra/module): make id use explicit args (#2509)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

modified theorem fderiv_id

modified theorem has_fderiv_at_id

deleted theorem has_strict_fderiv_at.snd

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_map.norm_id

modified theorem continuous_linear_map.norm_id_le

Modified src/geometry/manifold/basic_smooth_bundle.lean

Modified src/geometry/manifold/mfderiv.lean

modified theorem mfderiv_id

Modified src/topology/algebra/module.lean

modified theorem continuous_linear_map.coe_id'

modified theorem continuous_linear_map.coe_id

modified theorem continuous_linear_map.comp_id

modified theorem continuous_linear_map.id_apply

modified theorem continuous_linear_map.id_comp