Theorems · Theorem · number theory

MulChar.domRestrictHom_surjective

∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (N : Submonoid M), Function.Surjective ⇑(MulChar.domRestrictHom N R)

Let N be a submonoid of M group and let R be a ring with enough roots of unity. Then any R-value multiplicative character of N can be extended to a multiplicative character of M.

Defined in

Mathlib.NumberTheory.MulChar.Duality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidCommRingFiniteHasEnoughRootsOfUnity