Theorem CommGrp.μ_forget_apply

Modification history

2025-02-12 14:33

Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

feat(Algebra/Category): chosen finite products for group-like categories (#21737)

Added CommGrp.μ_forget_apply View on Github →