Zulip Chat Archive
Stream: mathlib4
Topic: docs4#Set.BijOn
Yaël Dillies (Jan 05 2023 at 12:20):
Shouldn't Set.BijOn rather be Set.bijOn?
Yaël Dillies (Jan 05 2023 at 12:20):
As Mario said earlier today, it's Int.natMod, not Int.NatMod.
Reid Barton (Jan 05 2023 at 12:28):
No because it returns a proposition, while Int.natMod returns a Nat.
Last updated: May 02 2025 at 03:31 UTC