Documentation

Mathlib.Init.Algebra.Classes

Unbundled algebra classes #

These classes are part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

By themselves, these classes are not good replacements for the Monoid / Group etc structures provided by mathlib, as they are not discoverable by simp unlike the current lemmas due to there being little to index on. The Wiki page linked above describes an algebraic normalizer, but it was never implemented in Lean 3.

Porting note: #

This file is ancient, and it would be good to replace it with a clean version that provides what mathlib4 actually needs.

I've omitted all the @[algebra] attributes, as they are not used elsewhere.

The section StrictWeakOrder has been omitted, but I've left the mathport output in place. Please delete if cleaning up.

I've commented out some classes which we think are completely unused in mathlib.

I've added many of the declarations to nolints.json. If you clean up this file, please add documentation to classes that we are keeping.

Mario made the following analysis of uses in mathlib3:

class IsSymmOp (α : Sort u) (β : Sort v) (op : ααβ) :
  • symm_op : ∀ (a b : α), op a b = op b a
Instances
    theorem IsSymmOp.symm_op {α : Sort u} {β : Sort v} {op : ααβ} [self : IsSymmOp α β op] (a : α) (b : α) :
    op a b = op b a
    @[reducible, inline, deprecated Std.Commutative]
    abbrev IsCommutative (α : Sort u) (op : ααα) :

    A commutative binary operation.

    Equations
    Instances For
      @[instance 100]
      instance isSymmOp_of_isCommutative (α : Sort u) (op : ααα) [Std.Commutative op] :
      IsSymmOp α α op
      Equations
      • =
      @[reducible, inline, deprecated Std.Associative]
      abbrev IsAssociative (α : Sort u) (op : ααα) :

      An associative binary operation.

      Equations
      Instances For
        @[reducible, inline, deprecated Std.LawfulLeftIdentity]
        abbrev IsLeftId (α : Sort u) (op : ααα) (o : outParam α) :

        A binary operation with a left identity.

        Equations
        Instances For
          @[reducible, inline, deprecated Std.LawfulRightIdentity]
          abbrev IsRightId (α : Sort u) (op : ααα) (o : outParam α) :

          A binary operation with a right identity.

          Equations
          Instances For
            class IsLeftCancel (α : Sort u) (op : ααα) :
            • left_cancel : ∀ (a b c : α), op a b = op a cb = c
            Instances
              theorem IsLeftCancel.left_cancel {α : Sort u} {op : ααα} [self : IsLeftCancel α op] (a : α) (b : α) (c : α) :
              op a b = op a cb = c
              class IsRightCancel (α : Sort u) (op : ααα) :
              • right_cancel : ∀ (a b c : α), op a b = op c ba = c
              Instances
                theorem IsRightCancel.right_cancel {α : Sort u} {op : ααα} [self : IsRightCancel α op] (a : α) (b : α) (c : α) :
                op a b = op c ba = c
                @[reducible, inline, deprecated Std.IdempotentOp]
                abbrev IsIdempotent (α : Sort u) (op : ααα) :
                Equations
                Instances For
                  class IsIrrefl (α : Sort u) (r : ααProp) :

                  IsIrrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

                  • irrefl : ∀ (a : α), ¬r a a
                  Instances
                    theorem IsIrrefl.irrefl {α : Sort u} {r : ααProp} [self : IsIrrefl α r] (a : α) :
                    ¬r a a
                    class IsRefl (α : Sort u) (r : ααProp) :

                    IsRefl X r means the binary relation r on X is reflexive.

                    • refl : ∀ (a : α), r a a
                    Instances
                      theorem IsRefl.refl {α : Sort u} {r : ααProp} [self : IsRefl α r] (a : α) :
                      r a a
                      class IsSymm (α : Sort u) (r : ααProp) :

                      IsSymm X r means the binary relation r on X is symmetric.

                      • symm : ∀ (a b : α), r a br b a
                      Instances
                        theorem IsSymm.symm {α : Sort u} {r : ααProp} [self : IsSymm α r] (a : α) (b : α) :
                        r a br b a
                        @[instance 100]
                        instance isSymmOp_of_isSymm (α : Sort u) (r : ααProp) [IsSymm α r] :

                        The opposite of a symmetric relation is symmetric.

                        Equations
                        • =
                        class IsAsymm (α : Sort u) (r : ααProp) :

                        IsAsymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

                        • asymm : ∀ (a b : α), r a b¬r b a
                        Instances
                          theorem IsAsymm.asymm {α : Sort u} {r : ααProp} [self : IsAsymm α r] (a : α) (b : α) :
                          r a b¬r b a
                          class IsAntisymm (α : Sort u) (r : ααProp) :

                          IsAntisymm X r means the binary relation r on X is antisymmetric.

                          • antisymm : ∀ (a b : α), r a br b aa = b
                          Instances
                            theorem IsAntisymm.antisymm {α : Sort u} {r : ααProp} [self : IsAntisymm α r] (a : α) (b : α) :
                            r a br b aa = b
                            @[instance 100]
                            instance IsAsymm.toIsAntisymm {α : Sort u} (r : ααProp) [IsAsymm α r] :
                            Equations
                            • =
                            class IsTrans (α : Sort u) (r : ααProp) :

                            IsTrans X r means the binary relation r on X is transitive.

                            • trans : ∀ (a b c : α), r a br b cr a c
                            Instances
                              theorem IsTrans.trans {α : Sort u} {r : ααProp} [self : IsTrans α r] (a : α) (b : α) (c : α) :
                              r a br b cr a c
                              instance instTransOfIsTrans {α : Sort u} {r : ααProp} [IsTrans α r] :
                              Trans r r r
                              Equations
                              • instTransOfIsTrans = { trans := }
                              @[instance 100]
                              instance instIsTransOfTrans {α : Sort u} {r : ααProp} [Trans r r r] :
                              IsTrans α r
                              Equations
                              • =
                              class IsTotal (α : Sort u) (r : ααProp) :

                              IsTotal X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

                              • total : ∀ (a b : α), r a b r b a
                              Instances
                                theorem IsTotal.total {α : Sort u} {r : ααProp} [self : IsTotal α r] (a : α) (b : α) :
                                r a b r b a
                                class IsPreorder (α : Sort u) (r : ααProp) extends IsRefl , IsTrans :

                                IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

                                  Instances
                                    class IsTotalPreorder (α : Sort u) (r : ααProp) extends IsTrans , IsTotal :

                                    IsTotalPreorder X r means that the binary relation r on X is total and a preorder.

                                      Instances
                                        @[instance 100]
                                        instance isTotalPreorder_isPreorder (α : Sort u) (r : ααProp) [s : IsTotalPreorder α r] :

                                        Every total pre-order is a pre-order.

                                        Equations
                                        • =
                                        class IsPartialOrder (α : Sort u) (r : ααProp) extends IsPreorder , IsAntisymm :

                                        IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and IsAntisymm X r.

                                          Instances
                                            class IsLinearOrder (α : Sort u) (r : ααProp) extends IsPartialOrder , IsTotal :

                                            IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and IsTotal X r.

                                              Instances
                                                class IsEquiv (α : Sort u) (r : ααProp) extends IsPreorder , IsSymm :

                                                IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and IsSymm X r.

                                                  Instances
                                                    class IsStrictOrder (α : Sort u) (r : ααProp) extends IsIrrefl , IsTrans :

                                                    IsStrictOrder X r means that the binary relation r on X is a strict order, that is, IsIrrefl X r and IsTrans X r.

                                                      Instances
                                                        class IsIncompTrans (α : Sort u) (lt : ααProp) :

                                                        IsIncompTrans X lt means that for lt a binary relation on X, the incomparable relation fun a b => ¬ lt a b ∧ ¬ lt b a is transitive.

                                                        • incomp_trans : ∀ (a b c : α), ¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a
                                                        Instances
                                                          theorem IsIncompTrans.incomp_trans {α : Sort u} {lt : ααProp} [self : IsIncompTrans α lt] (a : α) (b : α) (c : α) :
                                                          ¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a
                                                          class IsStrictWeakOrder (α : Sort u) (lt : ααProp) extends IsStrictOrder , IsIncompTrans :

                                                          IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and IsIncompTrans X lt.

                                                            Instances
                                                              class IsTrichotomous (α : Sort u) (lt : ααProp) :

                                                              IsTrichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

                                                              • trichotomous : ∀ (a b : α), lt a b a = b lt b a
                                                              Instances
                                                                theorem IsTrichotomous.trichotomous {α : Sort u} {lt : ααProp} [self : IsTrichotomous α lt] (a : α) (b : α) :
                                                                lt a b a = b lt b a
                                                                class IsStrictTotalOrder (α : Sort u) (lt : ααProp) extends IsTrichotomous , IsStrictOrder :

                                                                IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, IsTrichotomous X lt and IsStrictOrder X lt.

                                                                  Instances
                                                                    instance eq_isEquiv (α : Sort u) :
                                                                    IsEquiv α fun (x x_1 : α) => x = x_1

                                                                    Equality is an equivalence relation.

                                                                    Equations
                                                                    • =
                                                                    theorem irrefl {α : Sort u} {r : ααProp} [IsIrrefl α r] (a : α) :
                                                                    ¬r a a
                                                                    theorem refl {α : Sort u} {r : ααProp} [IsRefl α r] (a : α) :
                                                                    r a a
                                                                    theorem trans {α : Sort u} {r : ααProp} [IsTrans α r] {a : α} {b : α} {c : α} :
                                                                    r a br b cr a c
                                                                    theorem symm {α : Sort u} {r : ααProp} [IsSymm α r] {a : α} {b : α} :
                                                                    r a br b a
                                                                    theorem antisymm {α : Sort u} {r : ααProp} [IsAntisymm α r] {a : α} {b : α} :
                                                                    r a br b aa = b
                                                                    theorem asymm {α : Sort u} {r : ααProp} [IsAsymm α r] {a : α} {b : α} :
                                                                    r a b¬r b a
                                                                    theorem trichotomous {α : Sort u} {r : ααProp} [IsTrichotomous α r] (a : α) (b : α) :
                                                                    r a b a = b r b a
                                                                    theorem incomp_trans {α : Sort u} {r : ααProp} [IsIncompTrans α r] {a : α} {b : α} {c : α} :
                                                                    ¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
                                                                    @[instance 90]
                                                                    instance isAsymm_of_isTrans_of_isIrrefl {α : Sort u} {r : ααProp} [IsTrans α r] [IsIrrefl α r] :
                                                                    IsAsymm α r
                                                                    Equations
                                                                    • =
                                                                    @[elab_without_expected_type]
                                                                    theorem irrefl_of {α : Sort u} (r : ααProp) [IsIrrefl α r] (a : α) :
                                                                    ¬r a a
                                                                    @[elab_without_expected_type]
                                                                    theorem refl_of {α : Sort u} (r : ααProp) [IsRefl α r] (a : α) :
                                                                    r a a
                                                                    @[elab_without_expected_type]
                                                                    theorem trans_of {α : Sort u} (r : ααProp) [IsTrans α r] {a : α} {b : α} {c : α} :
                                                                    r a br b cr a c
                                                                    @[elab_without_expected_type]
                                                                    theorem symm_of {α : Sort u} (r : ααProp) [IsSymm α r] {a : α} {b : α} :
                                                                    r a br b a
                                                                    @[elab_without_expected_type]
                                                                    theorem asymm_of {α : Sort u} (r : ααProp) [IsAsymm α r] {a : α} {b : α} :
                                                                    r a b¬r b a
                                                                    @[elab_without_expected_type]
                                                                    theorem total_of {α : Sort u} (r : ααProp) [IsTotal α r] (a : α) (b : α) :
                                                                    r a b r b a
                                                                    @[elab_without_expected_type]
                                                                    theorem trichotomous_of {α : Sort u} (r : ααProp) [IsTrichotomous α r] (a : α) (b : α) :
                                                                    r a b a = b r b a
                                                                    @[elab_without_expected_type]
                                                                    theorem incomp_trans_of {α : Sort u} (r : ααProp) [IsIncompTrans α r] {a : α} {b : α} {c : α} :
                                                                    ¬r a b ¬r b a¬r b c ¬r c b¬r a c ¬r c a
                                                                    def StrictWeakOrder.Equiv {α : Sort u} {r : ααProp} (a : α) (b : α) :
                                                                    Equations
                                                                    Instances For
                                                                      theorem StrictWeakOrder.erefl {α : Sort u} {r : ααProp} [IsStrictWeakOrder α r] (a : α) :
                                                                      theorem StrictWeakOrder.esymm {α : Sort u} {r : ααProp} {a : α} {b : α} :
                                                                      theorem StrictWeakOrder.etrans {α : Sort u} {r : ααProp} [IsStrictWeakOrder α r] {a : α} {b : α} {c : α} :
                                                                      theorem StrictWeakOrder.not_lt_of_equiv {α : Sort u} {r : ααProp} {a : α} {b : α} :
                                                                      theorem StrictWeakOrder.not_lt_of_equiv' {α : Sort u} {r : ααProp} {a : α} {b : α} :
                                                                      instance StrictWeakOrder.isEquiv {α : Sort u} {r : ααProp} [IsStrictWeakOrder α r] :
                                                                      IsEquiv α StrictWeakOrder.Equiv
                                                                      Equations
                                                                      • =

                                                                      The equivalence relation induced by lt

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le : ααProp} {lt : ααProp} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ (a b : α), lt a b ¬le b a) :
                                                                        theorem lt_of_lt_of_incomp {α : Sort u} {lt : ααProp} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} :
                                                                        lt a b¬lt b c ¬lt c blt a c
                                                                        theorem lt_of_incomp_of_lt {α : Sort u} {lt : ααProp} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} :
                                                                        ¬lt a b ¬lt b alt b clt a c
                                                                        theorem eq_of_incomp {α : Sort u} {lt : ααProp} [IsTrichotomous α lt] {a : α} {b : α} :
                                                                        ¬lt a b ¬lt b aa = b
                                                                        theorem eq_of_eqv_lt {α : Sort u} {lt : ααProp} [IsTrichotomous α lt] {a : α} {b : α} :
                                                                        theorem incomp_iff_eq {α : Sort u} {lt : ααProp} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) :
                                                                        ¬lt a b ¬lt b a a = b
                                                                        theorem eqv_lt_iff_eq {α : Sort u} {lt : ααProp} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) :
                                                                        theorem not_lt_of_lt {α : Sort u} {lt : ααProp} [IsStrictOrder α lt] {a : α} {b : α} :
                                                                        lt a b¬lt b a