Zulip Chat Archive
Stream: Is there code for X?
Topic: zify and divisibility
Yaël Dillies (Feb 01 2022 at 07:38):
Is tactic#zify meant to be used for divisibility? If not, could it be extended to?
Kyle Miller (Feb 01 2022 at 07:57):
It looks like all you need to do is
attribute [zify] int.coe_nat_dvd
Kyle Miller (Feb 01 2022 at 07:58):
That made me wonder about MOD/ZMOD, and similarly it looks like all you'd need to do is
attribute [zify] int.coe_nat_modeq_iff
Kyle Miller (Feb 01 2022 at 21:31):
@Rob Lewis Would it make sense to globally add the zify attribute to these two lemmas?
Last updated: Dec 20 2023 at 11:08 UTC