Theorems · Theorem · number theory

MulChar.inv_apply

∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommMonoidWithZero R] (χ : MulChar R R')
  (a : R), χ⁻¹ a = χ (Ring.inverse a)

When the domain has a zero, then the inverse of a multiplicative character χ, applied to a, is χ applied to the inverse of a.

Defined in

Mathlib.NumberTheory.MulChar.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroCommMonoidWithZero