Documentation

Mathlib.Data.Finsupp.Notation

Notation for Finsupp #

This file provides fun₀ | 3 => a | 7 => b notation for Finsupp, which desugars to Finsupp.update and Finsupp.single, in the same way that {a, b} desugars to insert and singleton.

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

    fun₀ | i => a is notation for Finsupp.single i a, and with multiple match arms, fun₀ ... | i => a is notation for Finsupp.update (fun₀ ...) i a.

    As a result, if multiple match arms coincide, the last one takes precedence.

    If the expected type is Π₀ i, α i (DFinsupp) and Mathlib.Data.DFinsupp.Notation is imported, then this is notation for DFinsupp.single and Dfinsupp.update instead.

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

      Implementation detail for fun₀, used by both Finsupp and DFinsupp

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

        Implementation detail for fun₀, used by both Finsupp and DFinsupp

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

          Finsupp elaborator for single₀.

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

            Finsupp elaborator for update₀.

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

              Unexpander for the fun₀ | i => x notation.

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

                Unexpander for the fun₀ | i => x notation.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  unsafe instance Finsupp.instRepr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] [Zero β] :
                  Repr (α →₀ β)

                  Display Finsupp using fun₀ notation.