Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zmod.ring_char_zmod_n

Modification history

2022-04-26 17:50
src/data/zmod/basic.lean
refactor(number_theory/legendre_symbol/quadratic_reciprocity.lean): change definition of legendre_sym, simplify proofs, add lemmas (#13667) …
Added zmod.ring_char_zmod_nView on Github →