Documentation
AddCombi
.
Mathlib
.
Algebra
.
Notation
.
Indicator
Search
return to top
source
Imports
Init
Mathlib.Algebra.Notation.Indicator
Imported by
Indicator
.
«term𝟭_[_,_]»
Indicator
.
«term𝟭_[_]»
source
def
Indicator
.
«term𝟭_[_,_]»
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Indicator
.
«term𝟭_[_]»
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For