Basic

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

Statistics

Metric	Count
Definitions `isProductAt`, `inclusionLinearMap`, `indexSupport`, `mapAlongLinearMap`, `mulSingle`, `mulSupport`, `single`, `singleAddMonoidHom`, `structureMapAddMonoidHom`, `structureMapMonoidHom`, `structureMapRingHom`, `structureSubring`, `support`	13
Theorems `add_comm_of_disjoint_support`, `coe_comp_inclusion`, `components_comp_coe_eq_coe_apply`, `eventually_surjOn_of_surjective`, `exists_apply_eq`, `exists_update`, `image_coe_preimage_inclusion_subset`, `inclusion_apply`, `mapAlongLinearMap_apply`, `mem_coset_and_mulSupport_subset_of_isProductAt`, `mem_indexSupport_iff`, `mem_structureSubring_iff`, `mulSingle_eq_of_ne`, `mulSingle_eq_of_ne'`, `mulSingle_eq_one_iff`, `mulSingle_eq_same`, `mulSingle_inj`, `mulSingle_injective`, `mulSingle_mul`, `mulSingle_ne_one_iff`, `mulSingle_one`, `mulSupport_inv`, `mulSupport_mul_subset`, `mul_comm_of_disjoint_mulSupport`, `mul_single`, `not_mem_mulSupport`, `not_mem_support`, `single_add`, `single_eq_of_ne`, `single_eq_of_ne'`, `single_eq_same`, `single_eq_zero_iff`, `single_inj`, `single_injective`, `single_mul`, `single_ne_zero_iff`, `single_zero`, `support_add_subset`, `support_neg`, `surjective_components_of_surjective`, `inclusionLinearMap_apply`	41
Total	54

RestrictedProduct

Definitions

Name	Category	Theorems
`inclusionLinearMap` 📖	CompOp	5 math math: `instIsDirectLimit`, `instDirectedSystemCoeSubmoduleCoeLinearMapIdInclusionLinearMap`, `instDirectedSystemOrderDualElemSetSetsCoeSubmodulePrincipalValMemCoeLinearMapIdInclusionLinearMap`, `instIsDirectLimit'`, `inclusionLinearMap_apply`
`indexSupport` 📖	CompOp	1 math math: `mem_indexSupport_iff`
`mapAlongLinearMap` 📖	CompOp	1 math math: `mapAlongLinearMap_apply`
`mulSingle` 📖	CompOp	8 math math: `mulSingle_injective`, `mulSingle_eq_of_ne'`, `mulSingle_mul`, `mulSingle_one`, `mulSingle_inj`, `mulSingle_eq_of_ne`, `mulSingle_eq_same`, `mulSingle_eq_one_iff`
`mulSupport` 📖	CompOp	2 math math: `not_mem_mulSupport`, `mulSupport_inv`
`single` 📖	CompOp	14 math math: `single_injective`, `single_eq_zero_iff`, `single_mul`, `mul_single`, `single_zero`, `single_add`, `smul_single`, `single_smul`, `single_eq_smul`, `single_inj`, `linearMap_component_apply`, `single_eq_of_ne`, `single_eq_same`, `single_eq_of_ne'`
`singleAddMonoidHom` 📖	CompOp	—
`structureMapAddMonoidHom` 📖	CompOp	—
`structureMapMonoidHom` 📖	CompOp	—
`structureMapRingHom` 📖	CompOp	—
`structureSubring` 📖	CompOp	4 math math: `padic_exists_sub_mem_structureSubring`, `Rat.FiniteAdeleRing.padicEquiv_bijOn`, `mem_structureSubring_iff`, `RingEquiv.restrictedProductCongr_bijOn_structureSubring`
`support` 📖	CompOp	2 math math: `support_neg`, `not_mem_support`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_comm_of_disjoint_support` 📖	—	`support`	—	—	`not_mem_support`
`coe_comp_inclusion` 📖	—	—	—	—	—
`components_comp_coe_eq_coe_apply` 📖	—	—	—	—	—
`eventually_surjOn_of_surjective` 📖	—	—	—	—	—
`exists_apply_eq` 📖	—	—	—	—	`exists_update`
`exists_update` 📖	—	—	—	—	—
`image_coe_preimage_inclusion_subset` 📖	—	—	—	—	—
`inclusion_apply` 📖	—	—	—	—	—
`mapAlongLinearMap_apply` 📖	mathematical	—	`mapAlongLinearMap`	—	—
`mem_coset_and_mulSupport_subset_of_isProductAt` 📖	—	`SubmonoidClass.isProductAt` `mulSupport`	—	—	`mul_comm_of_disjoint_mulSupport` `mulSupport_inv` `mulSupport_mul_subset`
`mem_indexSupport_iff` 📖	mathematical	—	`indexSupport`	—	—
`mem_structureSubring_iff` 📖	mathematical	—	`structureSubring`	—	`structureSubring.eq_1`
`mulSingle_eq_of_ne` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_eq_of_ne'` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_eq_one_iff` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_eq_same` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_inj` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_injective` 📖	mathematical	—	`mulSingle`	—	—
`mulSingle_mul` 📖	mathematical	—	`mulSingle`	—	`mulSingle_eq_same` `mulSingle_eq_of_ne'`
`mulSingle_ne_one_iff` 📖	—	—	—	—	—
`mulSingle_one` 📖	mathematical	—	`mulSingle`	—	—
`mulSupport_inv` 📖	mathematical	—	`mulSupport`	—	—
`mulSupport_mul_subset` 📖	—	`mulSupport`	—	—	`not_mem_mulSupport`
`mul_comm_of_disjoint_mulSupport` 📖	—	`mulSupport`	—	—	`not_mem_mulSupport`
`mul_single` 📖	mathematical	—	`single`	—	`single_eq_same` `single_eq_of_ne'`
`not_mem_mulSupport` 📖	mathematical	—	`mulSupport`	—	—
`not_mem_support` 📖	mathematical	—	`support`	—	—
`single_add` 📖	mathematical	—	`single`	—	`single_eq_same` `single_eq_of_ne'`
`single_eq_of_ne` 📖	mathematical	—	`single`	—	—
`single_eq_of_ne'` 📖	mathematical	—	`single`	—	—
`single_eq_same` 📖	mathematical	—	`single`	—	—
`single_eq_zero_iff` 📖	mathematical	—	`single`	—	—
`single_inj` 📖	mathematical	—	`single`	—	—
`single_injective` 📖	mathematical	—	`single`	—	—
`single_mul` 📖	mathematical	—	`single`	—	`single_eq_same` `single_eq_of_ne'`
`single_ne_zero_iff` 📖	—	—	—	—	—
`single_zero` 📖	mathematical	—	`single`	—	—
`support_add_subset` 📖	—	`support`	—	—	`not_mem_support`
`support_neg` 📖	mathematical	—	`support`	—	—
`surjective_components_of_surjective` 📖	—	—	—	—	`exists_apply_eq`

RestrictedProduct.SubmonoidClass

Definitions

Name	Category	Theorems
`isProductAt` 📖	MathDef	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inclusionLinearMap_apply` 📖	mathematical	—	`RestrictedProduct.inclusionLinearMap`	—	—

---

← Back to Index