Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-16 06:06 f585ce54

View on Github →

feat(category_theory): monoidal natural transformations and discrete monoidal categories (#4112)

Estimated changes

Modified src/algebra/group/hom.lean

added theorem monoid_hom.congr_arg

added theorem monoid_hom.congr_fun

Modified src/algebra/group_with_zero.lean

modified theorem monoid_hom.map_div

Modified src/algebra/ring/basic.lean

added theorem ring_hom.congr_arg

added theorem ring_hom.congr_fun

Modified src/category_theory/discrete_category.lean

added theorem category_theory.discrete.eq_of_hom

Modified src/category_theory/limits/lattice.lean

Created src/category_theory/monoidal/discrete.lean

added def category_theory.discrete.monoidal_functor

added def category_theory.discrete.monoidal_functor_comp

Modified src/category_theory/monoidal/functor.lean

Modified src/category_theory/monoidal/internal.lean

added def category_theory.lax_monoidal_functor.map_Mon_functor

Created src/category_theory/monoidal/natural_transformation.lean

added def category_theory.monoidal_nat_trans.hcomp

added def category_theory.monoidal_nat_trans.id

added def category_theory.monoidal_nat_trans.vcomp

added structure category_theory.monoidal_nat_trans

Modified src/topology/instances/real_vector_space.lean