Theorems · Theorem · commutative algebra

Submodule.span_range_eq_top_of_injective_of_rank_le

∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {M N : Type u}
  [IsDomain R] [IsFractionRing R K] [inst_5 : AddCommGroup M] [inst_6 : Module R M] [inst_7 : AddCommGroup N]
  [inst_8 : Module R N] [inst_9 : Module K N] [IsScalarTower R K N] [Module.Finite K N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → Module.rank K N ≤ Module.rank R M → Submodule.span K ↑f.range = ⊤

Defined in

Mathlib.Algebra.Module.Lattice

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraIsDomainIsFractionRingAddCommGroupModuleAddCommGroupModuleModuleIsScalarTowerModule.Finite