Def Nat.totient

Modification history

2024-10-22 21:02

Mathlib/Data/Nat/Totient.lean

chore(Data): use newly introduced finset notation (#18059) …

Modified Nat.totient View on Github →

2023-03-29 05:37

Mathlib/Data/Nat/Totient.lean

feat: port Data.Nat.Totient (#3156)

Added Nat.totient View on Github →