Documentation Verification Report

TensorProduct

📁 Source: FLT/Mathlib/Topology/Algebra/Module/TensorProduct.lean

Statistics

Metric	Count
Definitions `chooseBasis_piScalarRight`, `chooseBasis_piScalarRight'`, `rTensor`	3
Theorems `rTensor_comp`, `rTensor_comp_apply`, `rTensor_id`, `rTensor_id_apply`	4
Total	7

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`chooseBasis_piScalarRight` 📖	CompOp	—
`chooseBasis_piScalarRight'` 📖	CompOp	6 math math: `basis_repr_eq`, `basis_eq_single_global`, `basis_eq`, `basis_eq_single`, `basis_repr_eq_global`, `basis_eq_global`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`rTensor` 📖	CompOp	5 math math: `rTensor_id`, `rTensor_id_apply`, `rTensor_comp_apply`, `IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply`, `rTensor_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rTensor_comp` 📖	mathematical	—	`rTensor`	—	`rTensor_comp_apply`
`rTensor_comp_apply` 📖	mathematical	—	`rTensor`	—	—
`rTensor_id` 📖	mathematical	—	`rTensor`	—	`rTensor_id_apply`
`rTensor_id_apply` 📖	mathematical	—	`rTensor`	—	—

---

← Back to Index