Theorem ZMod.eisenstein_lemma_aux

Modification history

2023-06-26 15:50

Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

feat: port NumberTheory.LegendreSymbol.GaussEisensteinLemmas (#5492)

Added ZMod.eisenstein_lemma_aux View on Github →