Documentation mistake in algebra.covariant_and_contravariant

Stream: mathlib4

[Itai Bar-Natan]

I haven't found contribution guidelines for reporting an issue without making a pull request. Sorry if this isn't the appropriate channel.

There's a mistake in the documentation of algebra.covariant_and_contravariant.covariant_class and algebra.covariant_and_contravariant.contravariant_class that is currently online (link). For both, the second paragraph describes the parameters of the class and incorrectly indicates the type of the relation r is N → Nwhen it is actually N → N → Prop, as seen in the type signature.

[Mario Carneiro]

For a simple documentation bug like this, I would just suggest making a PR for it, possibly using the "edit file" option in github if you don't have a mathlib contribution setup already. It will usually get merged without much fuss.

[Mario Carneiro]

(Also this is the mathlib4 stream; discussion about mathlib usually goes in #general , #new members or #maths)

[Itai Bar-Natan]

https://github.com/leanprover-community/mathlib/pull/9171

[Bryan Gin-ge Chen]

Thank you! I've put it on the queue.

For future reference, our guidelines for contributors can be found here.

[Notification Bot]

This topic was moved by Scott Morrison to #general > Documentation mistake in algebra.covariant_and_contravariant