Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.snd_inr

Modification history

2020-07-23 18:29

src/algebra/pi_instances.lean

refactor(algebra/pi_instance): delete pi_instance file, and move instances to group/ring etc appropriately (#3513)

Deleted prod.snd_inr View on Github →

2018-09-20 19:21

algebra/pi_instances.lean

refactor(algebra/pi_instances): move prod instances to pi_instances file

Modified prod.snd_inr View on Github →

2017-12-08 17:29

algebra/linear_algebra/prod_module.lean

feat(algebra/linear_algebra): add product construction for modules

Added prod.snd_inr View on Github →