Commit 2024-08-29 21:20 b280d919

View on Github →

feat(Data.ZMod): More lemmas about ZMod.val (#14327)

Estimated changes

Modified Mathlib/Combinatorics/Schnirelmann.lean

Modified Mathlib/Data/Nat/Defs.lean

added theorem Nat.one_mod_eq_one

modified theorem Nat.one_mod_of_ne_one

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.val_cast_zmod_lt

added theorem ZMod.val_eq_one

added theorem ZMod.val_mul_iff_lt

added theorem ZMod.val_pos

added theorem ZMod.val_pow

added theorem ZMod.val_pow_le

Modified scripts/style-exceptions.txt