# Order Monoid Isomorphisms on `Additive` and `Multiplicative`. #

source
def OrderMonoidIso.toAdditive {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] :
(G ≃*o H) ≃ (Additive G ≃+o Additive H)

Reinterpret `G ≃*o H` as `Additive G ≃+o Additive H`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def OrderAddMonoidIso.toMultiplicative {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(G ≃+o H) ≃ (Multiplicative G ≃*o Multiplicative H)

Reinterpret `G ≃+o H` as `Multiplicative G ≃*o Multiplicative H`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def OrderAddMonoidIso.toMultiplicativeRight {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(Additive G ≃+o H) ≃ (G ≃*o Multiplicative H)

Reinterpret `Additive G ≃+o H` as `G ≃*o Multiplicative H`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[deprecated OrderAddMonoidIso.toMultiplicativeRight (since := "2025-09-19")]
def OrderAddMonoidIso.toMultiplicative' {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(Additive G ≃+o H) ≃ (G ≃*o Multiplicative H)

Alias of `OrderAddMonoidIso.toMultiplicativeRight`.

Reinterpret `Additive G ≃+o H` as `G ≃*o Multiplicative H`.

Equations

- @OrderAddMonoidIso.toMultiplicative' = @OrderAddMonoidIso.toMultiplicativeRight

Instances For

source
@[reducible, inline]
abbrev OrderMonoidIso.toAdditiveLeft {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(G ≃*o Multiplicative H) ≃ (Additive G ≃+o H)

Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`.

Equations

- OrderMonoidIso.toAdditiveLeft = OrderAddMonoidIso.toMultiplicativeRight.symm

Instances For

source
@[deprecated OrderMonoidIso.toAdditiveLeft (since := "2025-09-19")]
def OrderMonoidIso.toAdditive' {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] :
(G ≃*o Multiplicative H) ≃ (Additive G ≃+o H)

Alias of `OrderMonoidIso.toAdditiveLeft`.

Reinterpret `G ≃* Multiplicative H` as `Additive G ≃+ H`.

Equations

- @OrderMonoidIso.toAdditive' = @OrderMonoidIso.toAdditiveLeft

Instances For

source
def OrderAddMonoidIso.toMultiplicativeLeft {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] :
(G ≃+o Additive H) ≃ (Multiplicative G ≃*o H)

Reinterpret `G ≃+o Additive H` as `Multiplicative G ≃*o H`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[deprecated OrderAddMonoidIso.toMultiplicativeLeft (since := "2025-09-19")]
def OrderAddMonoidIso.toMultiplicative'' {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] :
(G ≃+o Additive H) ≃ (Multiplicative G ≃*o H)

Alias of `OrderAddMonoidIso.toMultiplicativeLeft`.

Reinterpret `G ≃+o Additive H` as `Multiplicative G ≃*o H`.

Equations

- @OrderAddMonoidIso.toMultiplicative'' = @OrderAddMonoidIso.toMultiplicativeLeft

Instances For

source
@[reducible, inline]
abbrev OrderMonoidIso.toAdditiveRight {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] :
(Multiplicative G ≃*o H) ≃ (G ≃+o Additive H)

Reinterpret `Multiplicative G ≃*o H` as `G ≃+o Additive H` as.

Equations

- OrderMonoidIso.toAdditiveRight = OrderAddMonoidIso.toMultiplicativeLeft.symm

Instances For

source
@[deprecated OrderMonoidIso.toAdditiveRight (since := "2025-09-19")]
def OrderMonoidIso.toAdditive'' {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] :
(Multiplicative G ≃*o H) ≃ (G ≃+o Additive H)

Alias of `OrderMonoidIso.toAdditiveRight`.

Reinterpret `Multiplicative G ≃*o H` as `G ≃+o Additive H` as.

Equations

- @OrderMonoidIso.toAdditive'' = @OrderMonoidIso.toAdditiveRight

Instances For

source
def OrderMonoidIso.toMultiplicative_toAdditive {G : Type u_1} [CommMonoid G] [PartialOrder G] :
Multiplicative (Additive G) ≃*o G

The multiplicative version of an additivized ordered monoid is order-mul-equivalent to itself.

Equations

- OrderMonoidIso.toMultiplicative_toAdditive = OrderAddMonoidIso.toMultiplicativeLeft (OrderMonoidIso.toAdditive (OrderMonoidIso.refl G))

Instances For

source
def OrderAddMonoidIso.toAdditive_toMultiplicative {G : Type u_1} [AddCommMonoid G] [PartialOrder G] :
Additive (Multiplicative G) ≃+o G

The additive version of an multiplicativized ordered additive monoid is order-add-equivalent to itself.

Equations

- OrderAddMonoidIso.toAdditive_toMultiplicative = OrderMonoidIso.toAdditiveLeft (OrderAddMonoidIso.toMultiplicative (OrderAddMonoidIso.refl G))

Instances For

source
instance Additive.instUniqueOrderAddMonoidIso {G : Type u_1} {H : Type u_2} [CommMonoid G] [PartialOrder G] [CommMonoid H] [PartialOrder H] [Unique (G ≃*o H)] :
Unique (Additive G ≃+o Additive H)
Equations

- Additive.instUniqueOrderAddMonoidIso = OrderMonoidIso.toAdditive.symm.unique

source
instance Multiplicative.instUniqueOrderdMonoidIso {G : Type u_1} {H : Type u_2} [AddCommMonoid G] [PartialOrder G] [AddCommMonoid H] [PartialOrder H] [Unique (G ≃+o H)] :
Unique (Multiplicative G ≃*o Multiplicative H)
Equations

- Multiplicative.instUniqueOrderdMonoidIso = OrderAddMonoidIso.toMultiplicative.symm.unique