Documentation

Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder

Locally Finite Linearly Ordered Abelian Groups #

Main results #

theorem Finset.card_Ico_mul_right {M : Type u_1} [CancelCommMonoid M] [LinearOrder M] [IsOrderedMonoid M] [LocallyFiniteOrder M] [ExistsMulOfLE M] (a b c : M) :
(Ico (a * c) (b * c)).card = (Ico a b).card
theorem card_Ico_one_mul {M : Type u_1} [CancelCommMonoid M] [LinearOrder M] [IsOrderedMonoid M] [LocallyFiniteOrder M] [ExistsMulOfLE M] (a b : M) (ha : 1 a) (hb : 1 b) :
(Finset.Ico 1 (a * b)).card = (Finset.Ico 1 a).card + (Finset.Ico 1 b).card
theorem card_Ico_zero_add {M : Type u_1} [AddCancelCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] [LocallyFiniteOrder M] [ExistsAddOfLE M] (a b : M) (ha : 0 a) (hb : 0 b) :
(Finset.Ico 0 (a + b)).card = (Finset.Ico 0 a).card + (Finset.Ico 0 b).card

The canonical embedding (as a monoid hom) from a linearly ordered cancellative additive monoid into . This is either surjective or zero.

Equations
Instances For

    The canonical embedding (as an ordered monoid hom) from a linearly ordered cancellative group into . This is either surjective or zero.

    Equations
    Instances For

      Any nontrivial linearly ordered abelian group that is locally finite is isomorphic to .

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Any linearly ordered abelian group that is locally finite embeds into Multiplicative.

        Equations
        Instances For

          Any nontrivial linearly ordered abelian group with zero that is locally finite is isomorphic to ℤᵐ⁰.

          Equations
          Instances For

            Any linearly ordered abelian group with zero that is locally finite embeds into ℤᵐ⁰.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For