Theorem Submodule.exists_smith_normal_form_of_rank_eq

Modification history

2025-03-14 10:49
Mathlib/LinearAlgebra/FreeModule/PID.lean
refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank (#22902) …
Added Submodule.exists_smith_normal_form_of_rank_eqView on Github →