Sum

📁 Source: Mathlib/Data/Finite/Sum.lean

Statistics

Metric	Count
Definitions	0
Theorems instPSum, instSum, psum_left, psum_right, sum_left, sum_right	6
Total	6

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPSum 📖	mathematical	—	Finite	—	of_equiv instSum instFinitePLift
instSum 📖	mathematical	—	Finite	—	of_fintype
psum_left 📖	mathematical	—	Finite	—	of_injective PSum.inl_injective
psum_right 📖	mathematical	—	Finite	—	of_injective PSum.inr_injective
sum_left 📖	mathematical	—	Finite	—	of_injective Sum.inl_injective
sum_right 📖	mathematical	—	Finite	—	of_injective Sum.inr_injective

---

← Back to Index