Theorems · Definition · group theory

AddChar.mulShift

{R : Type u_1} → {M : Type u_2} → [inst : Ring R] → [inst_1 : CommMonoid M] → AddChar R M → R → AddChar R M

Define the multiplicative shift of an additive character. This satisfies mulShift ψ a x = ψ (a * x).

Defined in

Mathlib.Algebra.Group.AddChar

Cited by

26 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

RingCommMonoid