Commit 2021-10-31 11:57 e5f9becc
View on Github →chore(linear_algebra/basic): relax ring to semiring (#10030)
This relaxes a random selection of lemmas from ring R to semiring R, and cleans up some unused variables nearby.
Probably the most useful of these are submodule.mem_map_equiv, map_subtype.rel_iso, and submodule.disjoint_iff_comap_eq_bot