Commit 2021-08-12 13:21 f63c27b0

feat(linear_algebra): Smith normal form for submodules over a PID (#8588) This PR expands on submodule.basis_of_pid by showing that this basis can be chosen in "Smith normal form". That is: if M is a free module over a PID R and N ≤ M, then we can choose a basis bN for N and bM for M, such that the inclusion map from N to M expressed in these bases is a diagonal matrix in Smith normal form. The rather gnarly induction in the original submodule.basis_of_pid has been turned into an even gnarlier auxiliary lemma that does the inductive step (with the induction hypothesis broken into pieces so we can apply it part by part), followed by a re-proven submodule.basis_of_pid that picks out part of this inductive step. Then we feed the full induction hypothesis, along with submodule.basis_of_pid into the same induction again, to get submodule.exists_smith_normal_form_of_le, and from that we conclude our new results submodule.exists_smith_normal_form and ideal.exists_smith_normal_form.