Adjoining a zero/one to semigroups and related algebraic structures #
This file contains different results about adjoining an element to an algebraic structure which then
behaves like a zero or a one. An example is adjoining a one to a semigroup to obtain a monoid. That
this provides an example of an adjunction is proved in
Mathlib/Algebra/Category/MonCat/Adjunctions.lean
.
Another result says that adjoining to a group an element zero
gives a GroupWithZero
. For more
information about these structures (which are not that standard in informal mathematics, see
Mathlib/Algebra/GroupWithZero/Basic.lean
)
TODO #
WithOne.coe_mul
and WithZero.coe_mul
have inconsistent use of implicit parameters
@[simp]
theorem
WithZero.recZeroCoe_zero
{α : Type u}
{motive : WithZero α → Sort u_1}
(h₁ : motive 0)
(h₂ : (a : α) → motive ↑a)
:
@[simp]
theorem
WithZero.recZeroCoe_coe
{α : Type u}
{motive : WithZero α → Sort u_1}
(h₁ : motive 0)
(h₂ : (a : α) → motive ↑a)
(a : α)
: