Units (i.e., invertible elements) of a monoid #
An element of a Monoid
is a unit if it has a two-sided inverse.
Main declarations #
Units M
: the group of units (i.e., invertible elements) of a monoid.IsUnit x
: a predicate asserting thatx
is a unit (i.e., invertible element) of a monoid.
For both declarations, there is an additive counterpart: AddUnits
and IsAddUnit
.
See also Prime
, Associated
, and Irreducible
in Mathlib/Algebra/Associated.lean
.
Notation #
We provide Mˣ
as notation for Units M
,
resembling the notation $R^{\times}$ for the units of a ring, which is common in mathematics.
TODO #
The results here should be used to golf the basic Group
lemmas.
See Note [custom simps projection]
Equations
Instances For
See Note [custom simps projection]
Equations
Instances For
Units have decidable equality if the base Monoid
has decidable equality.
Equations
Additive units have decidable equality
if the base AddMonoid
has deciable equality.
Equations
Units of a monoid have a multiplication and multiplicative identity.
Equations
Additive units of an additive monoid have an addition and an additive identity.
Equations
Units of a monoid form a DivInvMonoid
.
Equations
Additive units of an additive monoid form a SubNegMonoid
.
Equations
Units of a commutative monoid form a commutative group.
Equations
Additive units of an additive commutative monoid form an additive commutative group.
Equations
Partial division, denoted a /ₚ u
. It is defined when the
second argument is invertible, and unlike the division operator
in DivisionRing
it is not totalized at zero.
Equations
Instances For
The element of the group of units, corresponding to an element of a monoid which is a unit. When
α
is a DivisionMonoid
, use IsUnit.unit'
instead.
Equations
Instances For
The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. When α
is a SubtractionMonoid
, use
IsAddUnit.addUnit'
instead.
Equations
Instances For
The element of the group of units, corresponding to an element of a monoid which is a unit. As
opposed to IsUnit.unit
, the inverse is computable and comes from the inversion on α
. This is
useful to transfer properties of inversion in Units α
to α
. See also toUnits
.
Equations
Instances For
The element of the additive group of additive units, corresponding to an element of
an additive monoid which is an additive unit. As opposed to IsAddUnit.addUnit
, the negation is
computable and comes from the negation on α
. This is useful to transfer properties of negation
in AddUnits α
to α
. See also toAddUnits
.
Equations
Instances For
Constructs a CommGroup
structure on a CommMonoid
consisting only of units.