Zulip Chat Archive
Stream: maths
Topic: class of primes
Johan Commelin (Jun 17 2019 at 10:35):
In data/padics/padic_norm.lean on L18 we find
attribute [class] nat.prime
Should this move to data/nat/prime.lean?
Scott Morrison (Jun 17 2019 at 11:06):
Doesn't seem unreasonable. (Or, if people don't like this, surely that should have been a local.)
Last updated: May 02 2025 at 03:31 UTC