mathlib3

635bc8db - feat(linear_algebra): membership of a submodule given a basis of the submodule (#17083)

feat(linear_algebra): membership of a submodule given a basis of the submodule (#17083) A selection of little lemmas on module bases needed for the absolute ideal norm. `basis.mem_submodule_iff` states: `x` is an element of a submodule `P` with basis iff `x` is a linear combination of basis vectors. We include the infinite and finite cases, and specialization to ideals. `basis.repr_sum_self` states that a linear combination of basis vectors has coordinates exactly given by the coefficient of the combination. This can almost already be done by `simp` except relating the finite sum to `finsupp.total`.