WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Finitary relation

Revision #1222 → #2908 · back to history

modifiedCharacteristic function of Rc5008b320b8f
FieldFrom #1222To #2908
mathlib.moduleMathlib.Algebra.IndicatorMathlib.Algebra.Notation.Indicator
addedCartesian product495f8e4c8ced
addedn-tuple61a992210b88
addedInfinitary relation6f82b819f174