mathlib3

f63c27b0 - feat(linear_algebra): Smith normal form for submodules over a PID (#8588)

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`.