Theorem CategoryTheory.Functor.map_inv'

Modification history

2026-04-09 16:23

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

feat(CategoryTheory/Monoidal): use to_additive for the Yoneda embedding of group objects (#37587)

Modified CategoryTheory.Functor.map_inv'View on Github →

2026-02-17 07:11

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

feat(AlgebraicGeometry): abelian varieties are abelian (#35354) …

Added CategoryTheory.Functor.map_inv'View on Github →