Theorems · Inductive type · number theory

MulChar

(R : Type u_1) → [CommMonoid R] → (R' : Type u_2) → [CommMonoidWithZero R'] → Type (max u_1 u_2)

Define a structure for multiplicative characters. A multiplicative character from a commutative monoid R to a commutative monoid with zero R' is a homomorphism of (multiplicative) monoids that sends non-units to zero.

Defined in

Mathlib.NumberTheory.MulChar.Basic

Cited by

186 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

CommMonoidCommMonoidWithZero