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):
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:
This should have a docstring saying "use the notation", right?
Last updated: May 02 2025 at 03:31 UTC