Commit 2024-07-30 08:33 7cd5c43f

View on Github →

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

Estimated changes

Modified Mathlib/NumberTheory/MulChar/Lemmas.lean

modified theorem MulChar.apply_mem_rootsOfUnity

modified theorem MulChar.exists_mulChar_orderOf_eq_card_units

Modified Mathlib/NumberTheory/NumberField/House.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean