Theorem MulChar.ringHomComp_one

Modification history

2024-07-15 18:29

Mathlib/NumberTheory/MulChar/Basic.lean

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

Added MulChar.ringHomComp_one View on Github →