Theorem AddChar.ringChar_ne

Modification history

2026-05-25 21:53
Mathlib/NumberTheory/LegendreSymbol/Complex.lean
chore(Mathlib/Tactic): stop norm_num importing the Bochner integral (#39602) …
Added AddChar.ringChar_neView on Github →