Pi

📁 Source: FLT/Mathlib/LinearAlgebra/Pi.lean

Statistics

Metric	Count
Definitions piScalarPiComm, piScalarPiCongrFiberwise, FiberwiseSMul	3
Theorems map_smul, map_smul'	2
Total	5

LinearEquiv

Definitions

Name	Category	Theorems
piScalarPiComm 📖	CompOp	—
piScalarPiCongrFiberwise 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
FiberwiseSMul 📖	CompData	1 math math: NumberField.InfiniteAdeleRing.instFiberwiseSMulInfinitePlaceCompletion

Pi.FiberwiseSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_smul 📖	—	—	—	—	map_smul'
map_smul' 📖	—	—	—	—	—

---

← Back to Index