Yury G. Kudryashov

Please don't do `map_inv`/`map_div`/`map_units_inv` in the same PR. I've started #15985 about these lemmas, and already fixed more files (also, my `map_units_inv` is more general).

I'll try to fix my branch while waiting for the next flight (I have about 4h).

My PR is ready.

@YaelDillies Could you please list API changes in the commit message?

Otherwise LGTM. Thanks! bors d+

Please add a `filter.has_basis` statement about your filter (comes from `at_top_basis.comap _`).

I'm on vacation for a few days. You may need to ping another maintainer if you want to have it reviewed earlier than July 6.

I was going to improve the linear algebra part of math-classes. In particular, it would be nice to just say "linear maps form a ring". Actually, I think that just...

Same as #482. Maybe, one of the issues should be closed. This one has more details.

There is a stub `transitivity` in `Tactic.Basic`. Probably, it should be removed. Also, could you please mark some lemmas as `@[symm]`/`@[trans]`?