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
Add an extra element 1
to a type
Add an extra element 0
to a type
Instances For
- WithZero.div
- WithZero.inhabited
- WithZero.instAdd
- WithZero.instAddCommMonoid
- WithZero.instAddMonoid
- WithZero.instAddMonoidWithOne
- WithZero.instAddZeroClass
- WithZero.instCanLift
- WithZero.instCanonicallyOrderedAdd
- WithZero.instCoeTC
- WithZero.instCommGroupWithZero
- WithZero.instCommMonoidWithZero
- WithZero.instCommSemigroup
- WithZero.instDivInvMonoid
- WithZero.instDivInvOneMonoid
- WithZero.instDivisionCommMonoid
- WithZero.instDivisionMonoid
- WithZero.instExistsAddOfLE
- WithZero.instGroupWithZero
- WithZero.instInvolutiveInv
- WithZero.instLattice
- WithZero.instLinearOrder
- WithZero.instLinearOrderedCommGroupWithZero
- WithZero.instLinearOrderedCommMonoidWithZero
- WithZero.instMonad
- WithZero.instMonoidWithZero
- WithZero.instMulLeftMono
- WithZero.instMulLeftReflectLT
- WithZero.instMulZeroClass
- WithZero.instMulZeroOneClass
- WithZero.instNeg
- WithZero.instNegZeroClass
- WithZero.instNoZeroDivisors
- WithZero.instNontrivial
- WithZero.instOrderBot
- WithZero.instPartialOrder
- WithZero.instPowInt
- WithZero.instPreorder
- WithZero.instRepr
- WithZero.instSemigroupWithZero
- WithZero.instZero
- WithZero.inv
- WithZero.invOneClass
- WithZero.isOrderedMonoid
- WithZero.one
- WithZero.pow
Equations
- WithZero.instRepr = { reprPrec := fun (o : WithZero α) (x : ℕ) => match o with | none => Std.Format.text "0" | some a => Std.Format.text "↑" ++ repr a }
Equations
- WithOne.instRepr = { reprPrec := fun (o : WithOne α) (x : ℕ) => match o with | none => Std.Format.text "1" | some a => Std.Format.text "↑" ++ repr a }
Equations
- WithOne.instOne = { one := none }
Equations
- WithZero.instZero = { zero := none }
Equations
- WithOne.instMul = { mul := Option.merge fun (x1 x2 : α) => x1 * x2 }
Equations
- WithZero.instAdd = { add := Option.merge fun (x1 x2 : α) => x1 + x2 }
Equations
- WithOne.instInv = { inv := fun (a : WithOne α) => Option.map Inv.inv a }
Equations
- WithZero.instNeg = { neg := fun (a : WithZero α) => Option.map Neg.neg a }
Equations
- WithOne.instInvOneClass = { toOne := WithOne.instOne, toInv := WithOne.instInv, inv_one := ⋯ }
Equations
- WithZero.instNegZeroClass = { toZero := WithZero.instZero, toNeg := WithZero.instNeg, neg_zero := ⋯ }
Equations
- WithOne.inhabited = { default := 1 }
Equations
- WithZero.inhabited = { default := 0 }
Equations
- WithOne.instCoeTC = { coe := WithOne.coe }
Equations
- WithZero.instCoeTC = { coe := WithZero.coe }
Recursor for WithZero
using the preferred forms 0
and ↑a
.
Equations
- WithZero.recZeroCoe zero coe none = zero
- WithZero.recZeroCoe zero coe (some a) = coe a
Recursor for WithOne
using the preferred forms 1
and ↑a
.
Equations
- WithOne.recOneCoe one coe none = one
- WithOne.recOneCoe one coe (some a) = coe a
Deconstruct an x : WithOne α
to the underlying value in α
, given a proof that x ≠ 1
.
Equations
- WithOne.unone x_3 = x_2
Deconstruct an x : WithZero α
to the underlying value in α
, given a proof that x ≠ 0
.
Equations
- WithZero.unzero x_3 = x_2
Equations
- One or more equations did not get rendered due to their size.
Equations
- WithOne.instCommMonoid = { toMonoid := WithOne.instMonoid, mul_comm := ⋯ }
Equations
- WithZero.instAddCommMonoid = { toAddMonoid := WithZero.instAddMonoid, add_comm := ⋯ }