Documentation Verification Report

Module

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

Statistics

Metric	Count
Definitions `restrictedProductPi`, `restrictedProductPi`, `instModuleCoe_fLT`, `instSMulCoe_fLT`, `linearMap_component`, `piSubringSubmodule`	6
Theorems `instContinuousSMulCoeCofinite_fLT`, `instContinuousSMulCoePrincipal_fLT`, `isModuleTopology`, `isOpenMap_linearMap_of_surjective`, `isOpen_piSubringSubmodule`, `linearMap_apply_eq_component`, `linearMap_component_apply`, `moduleToplogy_of_prod`, `single_eq_smul`, `single_smul`, `smul_apply'`, `smul_single`	12
Total	18

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`restrictedProductPi` 📖	CompOp	—

LinearEquiv

Definitions

Name	Category	Theorems
`restrictedProductPi` 📖	CompOp	—

RestrictedProduct

Definitions

Name	Category	Theorems
`instModuleCoe_fLT` 📖	CompOp	3 math math: `linearMap_apply_eq_component`, `linearMap_component_apply`, `isOpenMap_linearMap_of_surjective`
`instSMulCoe_fLT` 📖	CompOp	8 math math: `instContinuousSMulCoeCofinite_fLT`, `smul_single`, `single_smul`, `single_eq_smul`, `smul_apply'`, `isModuleTopology`, `instContinuousSMulCoePrincipal_fLT`, `moduleToplogy_of_prod`
`linearMap_component` 📖	CompOp	2 math math: `linearMap_apply_eq_component`, `linearMap_component_apply`
`piSubringSubmodule` 📖	CompOp	2 math math: `isOpen_piSubringSubmodule`, `moduleToplogy_of_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousSMulCoeCofinite_fLT` 📖	mathematical	—	`instSMulCoe_fLT`	—	`instContinuousSMulCoePrincipal_fLT`
`instContinuousSMulCoePrincipal_fLT` 📖	mathematical	—	`instSMulCoe_fLT`	—	`instContinuousSMulForall_fLT`
`isModuleTopology` 📖	mathematical	—	`instSMulCoe_fLT`	—	`moduleToplogy_of_prod` `IsModuleTopology.of_isOpenMap_surjective` `instContinuousSMulCoeCofinite_fLT` `isOpenMap_linearMap_of_surjective` `isOpen_piSubringSubmodule` `surjective_components_of_surjective` `linearMap_apply_eq_component` `eventually_surjOn_of_surjective`
`isOpenMap_linearMap_of_surjective` 📖	mathematical	`linearMap_component`	`instModuleCoe_fLT`	—	`isOpenMap_of_open_components` `linearMap_apply_eq_component`
`isOpen_piSubringSubmodule` 📖	mathematical	—	`piSubringSubmodule`	—	`piSubringSubmodule.eq_1`
`linearMap_apply_eq_component` 📖	mathematical	—	`instModuleCoe_fLT` `linearMap_component`	—	`linearMap_component_apply` `single_eq_smul` `single_smul` `single_eq_same`
`linearMap_component_apply` 📖	mathematical	—	`linearMap_component` `instModuleCoe_fLT` `single`	—	—
`moduleToplogy_of_prod` 📖	mathematical	—	`piSubringSubmodule` `instSMulCoe_fLT`	—	—
`single_eq_smul` 📖	mathematical	—	`instSMulCoe_fLT` `single`	—	`single_smul` `single.congr_simp`
`single_smul` 📖	mathematical	—	`instSMulCoe_fLT` `single`	—	`single_eq_same` `single_eq_of_ne'`
`smul_apply'` 📖	mathematical	—	`instSMulCoe_fLT`	—	—
`smul_single` 📖	mathematical	—	`instSMulCoe_fLT` `single`	—	`single_eq_same` `single_eq_of_ne'`

---

← Back to Index