Theorem MulChar.exists_mulChar_orderOf_eq_card_units

Modification history

2024-07-30 08:33

Mathlib/NumberTheory/MulChar/Lemmas.lean

chore(NumberTheory): drop some `DecidableEq` assumptions (#15288)

Modified MulChar.exists_mulChar_orderOf_eq_card_units View on Github →

2024-07-15 18:29

Mathlib/NumberTheory/MulChar/Lemmas.lean

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

Added MulChar.exists_mulChar_orderOf_eq_card_units View on Github →