Constructions

📁 Source: FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean

Statistics

Metric	Count
Definitions equivPi, finiteEquivPi	2
Theorems finiteEquivPi_symm_apply	1
Total	3

Module.Finite

Definitions

Name	Category	Theorems
equivPi 📖	CompOp	2 math math: NumberField.AdeleRing.piEquiv_apply_of_algebraMap, TensorProduct.AlgebraTensorModule.finiteEquivPi_symm_apply

TensorProduct.AlgebraTensorModule

Definitions

Name	Category	Theorems
finiteEquivPi 📖	CompOp	1 math math: finiteEquivPi_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteEquivPi_symm_apply 📖	mathematical	—	finiteEquivPi Module.Finite.equivPi	—	Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap

---

← Back to Index