Theorems · Theorem · number theory

IsCyclotomicExtension.equiv

∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {C : Type u_1}
  [inst_3 : CommRing C] [inst_4 : Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C),
  IsCyclotomicExtension S A C

Given (f : B ≃ₐ[A] C), if IsCyclotomicExtension S A B then IsCyclotomicExtension S A C.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraIsCyclotomicExtension