Documentation

LeanPool.PFR.AddCombi.Mathlib.Algebra.Notation.Indicator

Indicator notation #

source
def Indicator.«term𝟭_[_,_]» :
Lean.ParserDescr

Indicator-function notation with an explicit codomain.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Indicator.«term𝟭_[_]» :
    Lean.ParserDescr

    Indicator-function notation with an inferred codomain.

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