Prod

📁 Source: Mathlib/Data/Int/Cast/Prod.lean

Statistics

Metric	Count
Definitions instAddGroupWithOne	1
Theorems fst_intCast, snd_intCast	2
Total	3

Prod

Definitions

Name	Category	Theorems
instAddGroupWithOne 📖	CompOp	5 math math: fst_zmod_cast, fst_intCast, snd_zmod_cast, DoubleCentralizer.intCast_toProd, snd_intCast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fst_intCast 📖	mathematical	—	AddGroupWithOne.toIntCast instAddGroupWithOne	—	—
snd_intCast 📖	mathematical	—	AddGroupWithOne.toIntCast instAddGroupWithOne	—	—

---

← Back to Index