MulChar.restrictHom

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

{R : Type u_1} →
  [inst : CommMonoid R] →
    {S : Type u_3} →
      [inst_1 : SetLike S R] →
        [inst_2 : SubmonoidClass S R] →
          (T : S) → (R'' : Type u_4) → [inst_3 : CommMonoidWithZero R''] → MulChar R R'' →* MulChar (↥T) R''

Alias of MulChar.domRestrictHom. The restriction of a MulChar to a submonoid as an homomorphism.

Defined in: Mathlib.NumberTheory.MulChar.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommMonoid SetLike SubmonoidClass CommMonoidWithZero

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MonoidHomstatement · cited by 3,629
CommMonoidstatement · cited by 2,264
SetLikestatement · cited by 1,084
CommMonoidWithZerostatement · cited by 913
MulCharstatement · cited by 186
SubmonoidClassstatement · cited by 60
MulChar.domRestrictHomproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.