Documentation

Mathlib.Algebra.Notation

Notations for operations involving order and algebraic structure #

Notations #

class PosPart (α : Type u_1) :
Type u_1

A notation class for the positive part function: a⁺.

  • posPart : αα

    The positive part of an element a.

Instances
    class OneLePart (α : Type u_1) :
    Type u_1

    A notation class for the positive part function (multiplicative version): a⁺ᵐ.

    • oneLePart : αα

      The positive part of an element a.

    Instances
      class NegPart (α : Type u_1) :
      Type u_1

      A notation class for the negative part function: a⁻.

      • negPart : αα

        The negative part of an element a.

      Instances
        class LeOnePart (α : Type u_1) :
        Type u_1

        A notation class for the negative part function (multiplicative version): a⁻ᵐ.

        • leOnePart : αα

          The negative part of an element a.

        Instances

          The positive part of an element a.

          Equations
            Instances For

              The negative part of an element a.

              Equations
                Instances For

                  The positive part of an element a.

                  Equations
                    Instances For

                      The negative part of an element a.

                      Equations
                        Instances For