mathlib3 documentation

algebra.category.GroupWithZero

The category of groups with zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines GroupWithZero, the category of groups with zero.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def GroupWithZero.iso.mk {α β : GroupWithZero} (e : α ≃* β) :
α β

Constructs an isomorphism of groups with zero from a group isomorphism between them.

Equations
@[simp]
@[simp]