Theorems · Definition · number theory

MulChar.domRestrictHom

{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''

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

Defined in

Mathlib.NumberTheory.MulChar.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommMonoidSetLikeSubmonoidClassCommMonoidWithZero