mathlib

7e2084a7 - feat(linear_algebra): lemmas and instances on cardinality of quotients (#17084)

feat(linear_algebra): lemmas and instances on cardinality of quotients (#17084) * the quotient by the bottom submodule is infinite if the module is infinite * the quotient by the top submodule has a unique element (so it is finite), and this is the only submodule whose quotient has cardinality one * the quotient of a finite module is finite * the cardinality of a module is equal to the cardinality of a submodule times the cardinality of the quotient by that submodule * `[S : T] [M : S] = [M : T]` Bonus: `linear_equiv.of_subsingleton` states any two subsingleton modules are isomorphic (orignally used this, don't need it anymore but still seems useful).