Theorem ZMod.div_eq_filter_card

Modification history

2023-06-26 15:50

Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

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

Added ZMod.div_eq_filter_card View on Github →