Def MulChar.starComp

Modification history

2024-07-15 18:29

Mathlib/NumberTheory/MulChar/Lemmas.lean

feat(NumberTheory/MulChar): extend API for multiplicative characters (#13939) …

Added MulChar.starComp View on Github →