Theorems · Theorem · number theory

IsCyclotomicExtension.trans

∀ (S T : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (C : Type w)
  [inst_3 : CommRing C] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C]
  [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C],
  Function.Injective ⇑(algebraMap B C) → IsCyclotomicExtension (S ∪ T) A C

Transitivity of cyclotomic extensions.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTowerIsCyclotomicExtensionIsCyclotomicExtension