Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 17:49 56018332

View on Github →

chore(*): a few facts about pprod (#10519) Add equiv.pprod_equiv_prod and function.embedding.pprod_map.

Estimated changes

Modified src/data/equiv/basic.lean

added def equiv.pprod_equiv_prod

Modified src/data/pprod.lean

added theorem function.injective.pprod_map

Modified src/logic/embedding.lean

added def function.embedding.pprod_map