PProd

📁 Source: Mathlib/Data/Prod/PProd.lean

Statistics

Metric	Count
Definitions injArrow	1
Theorems pprod_map, exists, exists', forall, forall', eta	6
Total	7

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pprod_map 📖	—	—	—	—	—

PProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists 📖	—	—	—	—	—
exists' 📖	—	—	—	—	exists
forall 📖	—	—	—	—	—
forall' 📖	—	—	—	—	forall

PProd.mk

Definitions

Name	Category	Theorems
injArrow 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eta 📖	—	—	—	—	—

---

← Back to Index