Theorems · Theorem · number theory

IsCyclotomicExtension.le_of_dvd

∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B] (n₁ n₂ : ℕ)
  (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₂],
  n₁ ∣ n₂ → C₁ ≤ C₂

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsCyclotomicExtensionIsCyclotomicExtensionNeZero