Commit 2023-08-02 15:15 04c61390

View on Github →

refactor(Data/ZMod/Basic): Replace Fact ((n : ℕ) % 2 = 1) with Odd n (#6292) This PR replaces Fact ((n : ℕ) % 2 = 1) with Odd n, as suggested in #6086.

Estimated changes

Modified Mathlib/Data/ZMod/Basic.lean

modified theorem ZMod.ne_neg_self

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

modified theorem ZMod.gauss_lemma

modified theorem ZMod.gauss_lemma_aux