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: Dec 20 2023 at 11:08 UTC