Theorems · Theorem · number theory

IsCyclotomicExtension.finite

∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  [h₁ : Finite ↑S] [h₂ : IsCyclotomicExtension S A B], Module.Finite A B

If S is finite and IsCyclotomicExtension S A B, then B is a finite A-algebra.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainFiniteIsCyclotomicExtension