Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-17 10:20 896455c3

View on Github →

feat(category): add functor_norm simp_attr, and class is_comm_applicative

Estimated changes

Modified analysis/topology/continuity.lean

Modified analysis/topology/uniform_space.lean

Modified category/basic.lean

added theorem id_map'

added theorem is_comm_applicative.commutative_map

added theorem map_map

added theorem map_seq

added theorem pure_id'_seq

added theorem seq_map_assoc

Modified computability/partrec.lean

modified theorem partrec.comp