Theorems · Theorem · commutative algebra

Submodule.finiteQuotientOfFreeOfRankEq

∀ {M : Type u_3} [inst : AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (N : Submodule ℤ M),
  Module.finrank ℤ ↥N = Module.finrank ℤ M → Finite (M ⧸ N)

A submodule of full rank of a free finite ℤ-module has a finite quotient. It can't be an instance because of the side condition Module.finrank ℤ N = Module.finrank ℤ M.

Defined in

Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Cited by

3 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModule.FreeModule.Finite