Theorems · Theorem · number theory

IsCyclotomicExtension.finite_of_singleton

∀ (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsDomain B] [h : IsCyclotomicExtension {n} A B], Module.Finite A B

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NeZeroCommRingCommRingAlgebraIsDomainIsCyclotomicExtension