Theorems · Definition · number theory

restrictRootsOfUnity

{R : Type u_4} →
  {S : Type u_5} →
    {F : Type u_6} →
      [inst : CommMonoid R] →
        [inst_1 : CommMonoid S] →
          [inst_2 : FunLike F R S] → [MonoidHomClass F R S] → F → (n : ℕ) → ↥(rootsOfUnity n R) →* ↥(rootsOfUnity n S)

Restrict a ring homomorphism to the nth roots of unity.

Defined in

Mathlib.RingTheory.RootsOfUnity.Basic

Cited by

3 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext

Assumes

CommMonoidCommMonoidFunLikeMonoidHomClass