Skip to content

Conversation

@ctchou
Copy link
Contributor

@ctchou ctchou commented Oct 22, 2025

I just noticed that the Greek letter φ is used to denote the Euler totient function in the Nat namespace. Since the theory developed in Cslib/Foundations/Data/Nat/Segment.lean is also in the Nat namespace, its use of φ as a function name is potentially dangerous. This patch replaces all occurrences of φ by f and all previous occurrences of f by g.

@ctchou ctchou requested a review from fmontesi as a code owner October 22, 2025 01:43
@fmontesi fmontesi merged commit 7c752ca into leanprover:main Oct 23, 2025
4 checks passed
@ctchou ctchou deleted the chore-phi-to-f branch October 23, 2025 17:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants