Theorems · Theorem · field theory

Module.Finite.left

∀ (F : Type u) (K : Type v) (A : Type w) [inst : Ring F] [inst_1 : Ring K] [inst_2 : Module F K]
  [inst_3 : AddCommGroup A] [inst_4 : Module K A] [Module.IsTorsionFree K A] [inst_6 : Module F A] [IsNoetherian F A]
  [IsScalarTower F K A] [IsDomain K] [Nontrivial A], Module.Finite F K

In a tower of field extensions A / K / F, if A / F is finite, so is K / F. (In fact, it suffices that A is a nontrivial ring.) Note this cannot be an instance as Lean cannot infer A.

Defined in

Mathlib.FieldTheory.Tower

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingRingModuleAddCommGroupModuleModule.IsTorsionFreeModuleIsNoetherianIsScalarTowerIsDomainNontrivial