mathlib
47dbdaca - chore(data/support): move data/(support|indicator_function) to algebra/ (#7774)

Commit
4 years ago
chore(data/support): move data/(support|indicator_function) to algebra/ (#7774) These don't define any new structures, have not much to do with programming, and are just about basic features of algebraic gadgets, so belong better in `algebra/` than `data/`. See discussion of migrating content from `data/` to `algebra/` at [https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/move.20p-adics](zulip). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading