Theorems · Theorem · number theory

IsCyclotomicExtension.singleton_one_of_algebraMap_bijective

∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  Function.Surjective ⇑(algebraMap A B) → IsCyclotomicExtension {1} A B

If Function.Surjective (algebraMap A B), then IsCyclotomicExtension {1} A B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra