docs#int.nat_mod

Stream: mathlib4

[Yaël Dillies]

Where is docs#int.nat_mod gone? Context: #17896

[Niels Voss]

I think it went here, since the theorems seem similar nevermind, read the PR wrong
I think nat_mod was only used in 2 places in mathlib3, none of which are ported, and it was defined in core so the file was changed a lot

[Yaël Dillies]

What should I do? I am supposed to port a lemma about a definition that doesn't exist anymore :speechless:

[Mario Carneiro]

the definition exists, as I said on the issue, it's Int.natMod

[Mario Carneiro]

correction: it does not exist, it was planned to move from core to std but only the deletion from core was done

[Mario Carneiro]

The standard fix for a missing definition is to put it in the mathlib4 file corresponding to wherever it lived in lean 3

[Eric Wieser]

What file would that be for init.data.int.basic?

[Mario Carneiro]

Mathlib.Init.Data.Int.Basic

[Yaël Dillies]

Great, thanks!

[Eric Wieser]

Where do the #aligns live for the lemmas in that mathlib3 file?

[Mario Carneiro]

same place

[Eric Wieser]

Would it make sense to populate Mathlib.Init.Data.Int.Basic with an align for every mathlib3 declaration, even if the mathlib4 versions no longer live in that file?

[Mario Carneiro]

that too

[Mario Carneiro]

aligns always go there, the declaration also goes there if it hasn't been upstreamed

[Yaël Dillies]

Oh wait, it can't use % anymore, can it?

[Reid Barton]

Mod Int is overridden in Std.Data.Int.Basic to use the Lean 3 definition (at least if you're lucky and Lean picks the right instance)

[Yaël Dillies]

So I don't have to spell Int.emod out?

[Reid Barton]

I think that's right, you can and should just use %.