Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-07-16 12:59
844c665b
View on Github →
feat(category/applicative):
id
and
comp
functors; proofs by
norm
(
#184
)
Estimated changes
Created
category/applicative.lean
added
theorem
applicative.map_seq_map
added
theorem
applicative.pure_seq_eq_map'
added
theorem
comp.map_pure
added
theorem
comp.pure_seq_eq_map
added
theorem
comp.seq_assoc
added
theorem
comp.seq_mk
added
theorem
comp.seq_pure
Modified
category/basic.lean
deleted
theorem
map_map
deleted
def
mmap₂
added
def
mzip_with'
added
def
mzip_with
Created
category/functor.lean
added
theorem
functor.comp.map_mk
added
structure
functor.comp
added
theorem
functor.map_comp_map
added
theorem
functor.map_id
added
def
id.mk
Modified
data/prod.lean
Modified
data/set/basic.lean
Created
tactic/ext.lean
Modified
tactic/interactive.lean
Modified
tests/tactics.lean