Theorem AddChar.FiniteField.primitiveChar_to_Complex_isPrimitive

Modification history

2026-05-25 21:53
Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
chore(Mathlib/Tactic): stop norm_num importing the Bochner integral (#39602) …
Deleted AddChar.FiniteField.primitiveChar_to_Complex_isPrimitiveView on Github →
2024-05-31 13:35
Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
feat: add API for additive characters (#13389) …
Added AddChar.FiniteField.primitiveChar_to_Complex_isPrimitiveView on Github →