Documentation Verification Report

Equiv

📁 Source: FLT/Mathlib/Topology/Algebra/RestrictedProduct/Equiv.lean

Statistics

Metric	Count
Definitions `restrictedProductCongr`, `restrictedProductCongrLeft`, `restrictedProductCongrLeft'`, `restrictedProductCongrRight`, `restrictedProductCongr`, `restrictedProductCongrLeft`, `restrictedProductCongrLeft'`, `restrictedProductCongrRight`, `restrictedProductMatrix`, `restrictedProductPi`, `restrictedProductProd`, `Equiv`, `restrictedProductCongr`, `restrictedProductCongrLeft`, `restrictedProductCongrLeft'`, `restrictedProductCongrRight`, `restrictedProductCongr`, `restrictedProductCongrLeft`, `restrictedProductCongrLeft'`, `restrictedProductCongrRight`, `restrictedProductUnits`, `flatten`, `flatten_equiv`, `flatten_equiv'`, `principalAddEquivSum`, `principalEquivProd`, `principalLinearEquivProd`, `principalMulEquivProd`, `restrictedProductCongr`, `restrictedProductCongrLeft`, `restrictedProductCongrLeft'`, `restrictedProductCongrRight`	32
Theorems `restrictedProductCongrLeft'_apply`, `restrictedProductCongrRight_apply`, `restrictedProductCongr_apply`, `restrictedProductCongrLeft'_apply`, `restrictedProductCongrLeft'_symm_apply`, `restrictedProductCongrLeft'_symm_apply_apply`, `restrictedProductCongrLeft_apply_apply`, `restrictedProductCongrRight_apply`, `restrictedProductCongrRight_symm_apply`, `restrictedProductCongr_apply_apply`, `restrictedProductCongr_symm_apply`, `restrictedProductPi_symm_comp_inclusion`, `restrictedProductProd_apply`, `restrictedProductProd_symm_apply_coe`, `restrictedProductProd_symm_comp_inclusion`, `restrictedProductCongrLeft'_apply`, `restrictedProductCongrLeft'_apply`, `restrictedProductCongrRight_apply`, `restrictedProductCongr_apply`, `flatten_apply`, `flatten_equiv'_apply`, `flatten_equiv'_symm_apply`, `flatten_equiv_apply`, `flatten_equiv_symm_apply`, `restrictedProductCongrLeft'_apply`, `restrictedProductCongrRight_apply`, `restrictedProductCongr_apply_apply`, `restrictedProductCongr_bijOn_structureSubring`, `restrictedProductCongr_symm_apply`	29
Total	61

AddEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongr` 📖	CompOp	1 math math: `restrictedProductCongr_apply`
`restrictedProductCongrLeft` 📖	CompOp	—
`restrictedProductCongrLeft'` 📖	CompOp	1 math math: `restrictedProductCongrLeft'_apply`
`restrictedProductCongrRight` 📖	CompOp	1 math math: `restrictedProductCongrRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductCongrLeft'_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrRight_apply` 📖	mathematical	—	`restrictedProductCongrRight`	—	—
`restrictedProductCongr_apply` 📖	mathematical	—	`restrictedProductCongr` `Equiv.restrictedProductCongrLeft`	—	—

Equiv

Definitions

Name	Category	Theorems
`restrictedProductCongr` 📖	CompOp	2 math math: `restrictedProductCongr_apply_apply`, `restrictedProductCongr_symm_apply`
`restrictedProductCongrLeft` 📖	CompOp	3 math math: `MulEquiv.restrictedProductCongr_apply`, `AddEquiv.restrictedProductCongr_apply`, `restrictedProductCongrLeft_apply_apply`
`restrictedProductCongrLeft'` 📖	CompOp	3 math math: `restrictedProductCongrLeft'_apply`, `restrictedProductCongrLeft'_symm_apply_apply`, `restrictedProductCongrLeft'_symm_apply`
`restrictedProductCongrRight` 📖	CompOp	2 math math: `restrictedProductCongrRight_apply`, `restrictedProductCongrRight_symm_apply`
`restrictedProductMatrix` 📖	CompOp	1 math math: `Homeomorph.restrictedProductMatrix_toEquiv`
`restrictedProductPi` 📖	CompOp	3 math math: `restrictedProductPi_symm_comp_inclusion`, `continuous_restrictedProductPi`, `continuous_restrictedProductPi_symm`
`restrictedProductProd` 📖	CompOp	5 math math: `restrictedProductProd_apply`, `restrictedProductProd_symm_comp_inclusion`, `restrictedProductProd_symm_apply_coe`, `continuous_restrictedProductProd_symm`, `continuous_restrictedProductProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductCongrLeft'_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrLeft'_symm_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrLeft'_symm_apply_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrLeft_apply_apply` 📖	mathematical	—	`restrictedProductCongrLeft`	—	`restrictedProductCongrLeft'_symm_apply_apply`
`restrictedProductCongrRight_apply` 📖	mathematical	—	`restrictedProductCongrRight`	—	—
`restrictedProductCongrRight_symm_apply` 📖	mathematical	—	`restrictedProductCongrRight`	—	—
`restrictedProductCongr_apply_apply` 📖	mathematical	—	`restrictedProductCongr`	—	`restrictedProductCongrLeft_apply_apply`
`restrictedProductCongr_symm_apply` 📖	mathematical	—	`restrictedProductCongr`	—	—
`restrictedProductPi_symm_comp_inclusion` 📖	mathematical	—	`restrictedProductPi`	—	—
`restrictedProductProd_apply` 📖	mathematical	—	`restrictedProductProd`	—	—
`restrictedProductProd_symm_apply_coe` 📖	mathematical	—	`restrictedProductProd`	—	—
`restrictedProductProd_symm_comp_inclusion` 📖	mathematical	—	`restrictedProductProd`	—	—

IsDirectLimit

Definitions

Name	Category	Theorems
`Equiv` 📖	CompOp	2 math math: `Equiv_apply`, `linearEquiv_symm_apply`

LinearEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongr` 📖	CompOp	—
`restrictedProductCongrLeft` 📖	CompOp	—
`restrictedProductCongrLeft'` 📖	CompOp	1 math math: `restrictedProductCongrLeft'_apply`
`restrictedProductCongrRight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductCongrLeft'_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—

MulEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongr` 📖	CompOp	1 math math: `restrictedProductCongr_apply`
`restrictedProductCongrLeft` 📖	CompOp	—
`restrictedProductCongrLeft'` 📖	CompOp	1 math math: `restrictedProductCongrLeft'_apply`
`restrictedProductCongrRight` 📖	CompOp	1 math math: `restrictedProductCongrRight_apply`
`restrictedProductUnits` 📖	CompOp	2 math math: `MeasureTheory.ringHaarChar_restrictedProduct`, `MeasureTheory.ringHaarChar_adeles_rat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductCongrLeft'_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrRight_apply` 📖	mathematical	—	`restrictedProductCongrRight`	—	—
`restrictedProductCongr_apply` 📖	mathematical	—	`restrictedProductCongr` `Equiv.restrictedProductCongrLeft`	—	—

RestrictedProduct

Definitions

Name	Category	Theorems
`flatten` 📖	CompOp	1 math math: `flatten_apply`
`flatten_equiv` 📖	CompOp	2 math math: `flatten_equiv_symm_apply`, `flatten_equiv_apply`
`flatten_equiv'` 📖	CompOp	2 math math: `flatten_equiv'_apply`, `flatten_equiv'_symm_apply`
`principalAddEquivSum` 📖	CompOp	—
`principalEquivProd` 📖	CompOp	—
`principalLinearEquivProd` 📖	CompOp	—
`principalMulEquivProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flatten_apply` 📖	mathematical	—	`flatten`	—	—
`flatten_equiv'_apply` 📖	mathematical	—	`flatten_equiv'`	—	—
`flatten_equiv'_symm_apply` 📖	mathematical	—	`flatten_equiv'`	—	—
`flatten_equiv_apply` 📖	mathematical	—	`flatten_equiv`	—	—
`flatten_equiv_symm_apply` 📖	mathematical	—	`flatten_equiv`	—	—

RingEquiv

Definitions

Name	Category	Theorems
`restrictedProductCongr` 📖	CompOp	3 math math: `restrictedProductCongr_symm_apply`, `restrictedProductCongr_apply_apply`, `restrictedProductCongr_bijOn_structureSubring`
`restrictedProductCongrLeft` 📖	CompOp	—
`restrictedProductCongrLeft'` 📖	CompOp	1 math math: `restrictedProductCongrLeft'_apply`
`restrictedProductCongrRight` 📖	CompOp	1 math math: `restrictedProductCongrRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictedProductCongrLeft'_apply` 📖	mathematical	—	`restrictedProductCongrLeft'`	—	—
`restrictedProductCongrRight_apply` 📖	mathematical	—	`restrictedProductCongrRight`	—	—
`restrictedProductCongr_apply_apply` 📖	mathematical	—	`restrictedProductCongr`	—	`Equiv.restrictedProductCongrLeft_apply_apply`
`restrictedProductCongr_bijOn_structureSubring` 📖	mathematical	—	`restrictedProductCongr` `RestrictedProduct.structureSubring`	—	`RestrictedProduct.mem_structureSubring_iff` `restrictedProductCongr_apply_apply`
`restrictedProductCongr_symm_apply` 📖	mathematical	—	`restrictedProductCongr`	—	—

---

← Back to Index