Zulip Chat Archive

Stream: new members

Topic: How to represent the inverse of a mod n in Lean


Jiatong Yang (Dec 07 2024 at 06:35):

How to represent a^(-1) mod n in Lean?

Yaël Dillies (Dec 07 2024 at 07:48):

What do you want the types of a and a^(-1) mod n to be?

Jiatong Yang (Dec 07 2024 at 07:57):

a^(-1) mod n is a member of ZMod n

Daniel Weber (Dec 07 2024 at 07:58):

docs#ZMod.inv

Yaël Dillies (Dec 07 2024 at 08:03):

So yes can you simply use a⁻¹?

Eric Wieser (Dec 07 2024 at 17:51):

Daniel Weber said:

docs#ZMod.inv

This should have a docstring saying "use the notation", right?


Last updated: May 02 2025 at 03:31 UTC