embeddingsEquivPrimitiveRoots_apply_coe

English

The same embedding-application commutes with the coercions, giving the same evaluation value.

Русский

То же самое отображает сопоставление значений через обращение к вложениям и приведение к нормальным значениям.

LaTeX

$$$\text{embeddingsEquivPrimitiveRoots_apply_coe}$$$

Lean4

@[simp]
theorem embeddingsEquivPrimitiveRoots_apply_coe (C : Type*) [CommRing C] [IsDomain C] [Algebra K C]
    (hirr : Irreducible (cyclotomic n K)) (φ' : L →ₐ[K] C) : (hζ.embeddingsEquivPrimitiveRoots C hirr φ' : C) = φ' ζ :=
  rfl

Похожие утверждения