Documentation Verification Report

TensorProduct

📁 Source: FLT/DedekindDomain/FiniteAdeleRing/TensorProduct.lean

Statistics

Metric	Count
Definitions `localcomponent`, `localcomponentEquiv`	2
Theorems `localcomponent_apply`, `localcomponent_comp_apply`, `localcomponent_id_apply`	3
Total	5

IsDedekindDomain.FiniteAdeleRing.TensorProduct

Definitions

Name	Category	Theorems
`localcomponent` 📖	CompOp	3 math math: `localcomponent_id_apply`, `localcomponent_comp_apply`, `localcomponent_apply`
`localcomponentEquiv` 📖	CompOp	3 math math: `localcomponent_mulLeft`, `localcomponent_mulRight`, `FiniteAdeleRing.Aux.f_g_local_global`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`localcomponent_apply` 📖	mathematical	—	`ContinuousLinearMap.rTensor` `IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap` `localcomponent`	—	`ContinuousLinearMap.rTensor_comp_apply` `IsDedekindDomain.FiniteAdeleRing.singleContinuousAlgebraMap_comp_evalContinuousLinearMap` `IsDedekindDomain.FiniteAdeleRing.eval_localIdempotent`
`localcomponent_comp_apply` 📖	mathematical	—	`localcomponent`	—	`IsDedekindDomain.FiniteAdeleRing.singleContinuousAlgebraMap_comp_evalContinuousLinearMap` `IsDedekindDomain.FiniteAdeleRing.eval_localIdempotent`
`localcomponent_id_apply` 📖	mathematical	—	`localcomponent`	—	`IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap_singleContinuousLinearMap`

---

← Back to Index