mathlib3 documentation

ring_theory.zmod

Ring theoretic facts about zmod n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We collect a few facts about zmod n that need some ring theory to be proved/stated

Main statements #

@[simp]
theorem is_reduced_zmod {n : } :
@[protected, instance]