Mathlib v3 is deprecated. Go to Mathlib v4

Def function.embedding.pprod_map

Modification history

2021-11-29 17:49
src/logic/embedding.lean
chore(*): a few facts about `pprod` (#10519) …
Added function.embedding.pprod_mapView on Github →