Commit 2024-11-14 09:20 4bd54c44

feat(LinearAlgebra/FreeModule/Int): index of submodules of free ℤ-modules (#18002) Add some versions of the lemma that a submodule of a finite-dimensional free ℤ-module is a subgroup of finite index if and only if it's isomorphic to the original module. The version I actually have a use for is the final multiplicative version:

lemma subgroup_index_ne_zero_iff {m : ℕ} {H : Subgroup (Fin m → Multiplicative ℤ)} :
    H.index ≠ 0 ↔ Nonempty (H ≃* (Fin m → Multiplicative ℤ)) := by

From AperiodicMonotilesLean.