basic): delete useless defs and lemmas

Commit

2 years ago

chore(data/is_R_or_C/basic): delete useless defs and lemmas These are duplicates of more general versions

References

Author

eric-wieser

Parents