Theorems · Theorem · number theory

MulChar.restrictHom_surjective

Deprecated since 2026-07-19Use MulChar.domRestrictHom_surjective instead.

∀ (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)

Alias of MulChar.domRestrictHom_surjective. 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

0 results in Mathlib

Foundations

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

Assumes

CommMonoidCommRingFiniteHasEnoughRootsOfUnity