chore(algebra/char_zero): split (#17760)
Split `algebra/char_zero` into `algebra/char_zero/lemmas` and `algebra/char_zero/infinite` (there was already a `algebra/char_zero/defs`), with the former not importing finset.
As intended, this caused a few files which had been getting their finset import by this path to require that import explicitly. I've added the finset imports explicitly on all such files, except for `tactic/positivity`, the point being that I actually want to remove the finset import from positivity. I moved the `fin{set,type}.card` positivity extensions from `tactic/positivity` to `data/fintype/card`.
