Theorem Nat.one_mod_of_ne_one

Modification history

2024-08-29 21:20

Mathlib/Data/Nat/Defs.lean

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

Modified Nat.one_mod_of_ne_one View on Github →

2024-03-26 23:09

Mathlib/Data/Nat/Defs.lean

chore(Data/Nat): Use Std lemmas (#11661) …

Modified Nat.one_mod_of_ne_one View on Github →

2023-12-13 08:05

Mathlib/Data/Nat/Order/Basic.lean

feat(Combinatorics): definition and basic properties of Schnirelmann density (#7342) …

Added Nat.one_mod_of_ne_one View on Github →