Zulip Chat Archive
Stream: general
Topic: attribute [class] nat.prime
Kenny Lau (Oct 17 2018 at 07:52):
What is attribute [class] nat.prime
doing in padic_norm.lean
Johan Commelin (Oct 17 2018 at 07:54):
Waiting for someone to move it?
Last updated: May 02 2025 at 03:31 UTC