Documentation Verification Report

TensorRestrictedProduct

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

Statistics

Metric	Count
Definitions `lTensor`, `lTensorEquiv`, `lTensorPrincipalEquiv`, `rangeLTensor`, `tmulEquivRangeLTensor`	5
Theorems `lTensorEquiv_tmul`, `lTensorPrincipalEquiv_tmul`, `lTensor_bijective`, `lTensor_tmul`	4
Total	9

RestrictedProduct

Definitions

Name	Category	Theorems
`lTensor` 📖	CompOp	2 math math: `lTensor_tmul`, `lTensor_bijective`
`lTensorEquiv` 📖	CompOp	1 math math: `lTensorEquiv_tmul`
`lTensorPrincipalEquiv` 📖	CompOp	1 math math: `lTensorPrincipalEquiv_tmul`
`rangeLTensor` 📖	CompOp	7 math math: `lTensorEquiv_tmul`, `lTensor_tmul`, `IsDedekindDomain.range_adicCompletionTensorIntegerCoe_eq_lTensorRestriction`, `IsDedekindDomain.FiniteAdeleRing.tensorEquivRestrictedProduct_tmul`, `lTensorPrincipalEquiv_tmul`, `IsDedekindDomain.FiniteAdeleRing.restrictedProduct_tensorProduct_equiv_restrictedProduct_prod_apply`, `lTensor_bijective`
`tmulEquivRangeLTensor` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lTensorEquiv_tmul` 📖	mathematical	—	`rangeLTensor` `lTensorEquiv`	—	—
`lTensorPrincipalEquiv_tmul` 📖	mathematical	—	`rangeLTensor` `lTensorPrincipalEquiv`	—	—
`lTensor_bijective` 📖	mathematical	—	`rangeLTensor` `lTensor`	—	`instDirectedSystemOrderDualElemSetSetsCoeSubmodulePrincipalValMemCoeLinearMapIdInclusionLinearMap` `directed` `instIsDirectLimit'` `IsDirectLimit.Module.instDirectLimitCoeLinearMapIdOfOfNonempty` `instNonemptyOrderDualElemSetSets_fLT` `lTensorPrincipalEquiv_tmul` `IsDirectLimit.Module.linearEquiv_symm_apply`
`lTensor_tmul` 📖	mathematical	—	`rangeLTensor` `lTensor`	—	—

---

← Back to Index