restrictRootsOfUnity_coe_apply — Mathlib

English

The natural map that sends a root-of-unity in R to its image in S under a monoid homomorphism σ has its underlying unit in S given by σ evaluated on the corresponding unit in R.

Русский

Естественное отображение, отправляющее корень единства в R в его образ в S под гомоморфизмом σ, имеет основание-юнит в S, равное σ(соответствующий единичный элемент в R).

LaTeX

$$$(\restrictRootsOfUnity\ σ\ k\ ζ : S^{\times}) = σ(ζ : R^{\times}).$$$

Lean4

@[simp]
theorem restrictRootsOfUnity_coe_apply [MonoidHomClass F R S] (σ : F) (ζ : rootsOfUnity k R) :
    (restrictRootsOfUnity σ k ζ : Sˣ) = σ (ζ : Rˣ) :=
  rfl

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