mathlib documentation

algebra.category.GroupWithZero

The category of groups with zero #

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

@[protected, instance]
Equations
def GroupWithZero.of (α : Type u_1) [group_with_zero α] :

Construct a bundled GroupWithZero from a group_with_zero.

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]