The category of groups with zero #
This file defines GrpWithZero
, the category of groups with zero.
The category of groups with zero.
Equations
Instances For
Construct a bundled GrpWithZero
from a GroupWithZero
.
Instances For
Equations
- GrpWithZero.instInhabited = { default := GrpWithZero.of (WithZero PUnit.{?u.3 + 1}) }
Equations
- GrpWithZero.instFunLikeHomαGroupWithZero = { coe := fun (f : M ⟶ N) => (↑f).toFun, coe_injective' := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Constructs an isomorphism of groups with zero from a group isomorphism between them.
Equations
- GrpWithZero.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]