Theorems · Theorem · linear algebra

Submodule.finrank_span_eq_finrank_span

∀ (R : Type u_1) (A : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [Nontrivial A]
  [inst_3 : Algebra R A] [Algebra.IsEpi R A] [Module.Flat R A] [inst_6 : AddCommGroup M] [inst_7 : Module R M]
  [inst_8 : Module A M] [IsScalarTower R A M] [IsPrincipalIdealRing R] [IsDomain R] [Module.IsTorsionFree R M]
  (s : Set M) [Module.Finite R ↥(Submodule.span R s)],
  Module.finrank A ↥(Submodule.span A s) = Module.finrank R ↥(Submodule.span R s)

Defined in

Mathlib.LinearAlgebra.Span.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingNontrivialAlgebraAlgebra.IsEpiModule.FlatAddCommGroupModuleModuleIsScalarTowerIsPrincipalIdealRingIsDomainModule.IsTorsionFreeModule.Finite