Documentation

Mathlib.Algebra.Order.Hom.TypeTags

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.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)

      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
        @[reducible, inline]
        abbrev 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)

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

        Equations
        Instances For
          source
          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)

          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
            @[reducible, inline]
            abbrev 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)

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

            Equations
            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
              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
                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
                  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