Theorems · Theorem · field theory

Module.Finite.right

∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : Module F K]
  [inst_3 : AddCommMonoid A] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [hf : Module.Finite F A],
  Module.Finite K A

[Stacks Tag 09G5](https://stacks.math.columbia.edu/tag/09G5)

Defined in

Mathlib.FieldTheory.Tower

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringSemiringModuleAddCommMonoidModuleModuleIsScalarTowerModule.Finite