Theorems · Theorem · commutative algebra

Module.Finite.of_finite_tensorProduct_of_faithfullyFlat

∀ {R : Type u_1} [inst : CommRing R] (T : Type u_3) [inst_1 : CommRing T] [inst_2 : Algebra R T] {M : Type u_4}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.FaithfullyFlat R T] [Module.Finite T (TensorProduct R T M)],
  Module.Finite R M

Defined in

Mathlib.RingTheory.Finiteness.Descent

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAddCommGroupModuleModule.FaithfullyFlatModule.Finite