Theorems · Theorem · group theory

AddChar.mulShift_mul

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (r s : R),
  ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)

The product of mulShift ψ r and mulShift ψ s is mulShift ψ (r + s).

Defined in

Mathlib.Algebra.Group.AddChar

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingCommMonoid