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.

    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.instReprFinsupp {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] [Zero β] :
          Repr (α →₀ β)

          Display Finsupp using fun₀ notation.

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