Zulip Chat Archive
Stream: mathlib4
Topic: div_def
Scott Morrison (Dec 12 2022 at 08:19):
Would someone be interested in porting div_def, which is a missing TODO in Mathlib.Init.Data.Nat.Lemmas?
Scott Morrison (Dec 12 2022 at 08:20):
It is needed in mathlib4#927, so feel free to do it directly there.
Ruben Van de Velde (Dec 12 2022 at 08:21):
I can take a look - where should it go?
Ruben Van de Velde (Dec 12 2022 at 08:36):
Actually, it's called Nat.div_eq now
Last updated: Dec 20 2023 at 11:08 UTC