Theorems · Theorem · number theory

MulChar.equivToUnitHom_mul_apply

∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ₁ χ₂ : MulChar R R') (a : Rˣ),
  (MulChar.equivToUnitHom (χ₁ * χ₂)) a = (MulChar.equivToUnitHom χ₁) a * (MulChar.equivToUnitHom χ₂) a

Defined in

Mathlib.NumberTheory.MulChar.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidWithZero