Documentation Verification Report

PontryaginDual

📁 Source: Mathlib/Topology/Algebra/PontryaginDual.lean

Statistics

Metric	Count
Definitions `PontryaginDual`, `instCommGroup`, `instCompactSpaceOfDiscreteTopology`, `instContinuousMapClassCircle`, `instFunLikeCircle`, `instInhabited`, `instIsTopologicalGroup`, `instMonoidHomClassCircle`, `instT2Space`, `map`, `mapHom`, `instTopologicalSpacePontryaginDual`	12
Theorems `map_apply`, `map_comp`, `map_mul`, `map_one`, `instLocallyCompactSpacePontryaginDual`	5
Total	17

PontryaginDual

Definitions

Name	Category	Theorems
`instCommGroup` 📖	CompOp	4 math math: `map_one`, `map_mul`, `map_apply`, `map_comp`
`instCompactSpaceOfDiscreteTopology` 📖	CompOp	—
`instContinuousMapClassCircle` 📖	CompOp	—
`instFunLikeCircle` 📖	CompOp	1 math math: `map_apply`
`instInhabited` 📖	CompOp	—
`instIsTopologicalGroup` 📖	CompOp	1 math math: `map_mul`
`instMonoidHomClassCircle` 📖	CompOp	—
`instT2Space` 📖	CompOp	—
`map` 📖	CompOp	4 math math: `map_one`, `map_mul`, `map_apply`, `map_comp`
`mapHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_apply` 📖	mathematical	—	`DFunLike.coe` `PontryaginDual` `Circle` `instFunLikeCircle` `ContinuousMonoidHom` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `instTopologicalSpacePontryaginDual` `ContinuousMonoidHom.instFunLike` `map`	—	—
`map_comp` 📖	mathematical	—	`map` `ContinuousMonoidHom.comp` `PontryaginDual` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `instTopologicalSpacePontryaginDual`	—	`ContinuousMonoidHom.ext`
`map_mul` 📖	mathematical	—	`map` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `ContinuousMonoidHom` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ContinuousMonoidHom.instCommGroup` `PontryaginDual` `instCommGroup` `instTopologicalSpacePontryaginDual` `instIsTopologicalGroup`	—	`ContinuousMonoidHom.ext` `map_mul` `MonoidHomClass.toMulHomClass`
`map_one` 📖	mathematical	—	`map` `ContinuousMonoidHom` `ContinuousMonoidHom.instOne` `PontryaginDual` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `instCommGroup` `instTopologicalSpacePontryaginDual`	—	`ContinuousMonoidHom.ext` `OneHomClass.map_one` `MonoidHomClass.toOneHomClass`

(root)

Definitions

Name	Category	Theorems
`PontryaginDual` 📖	CompOp	5 math math: `PontryaginDual.map_one`, `PontryaginDual.map_mul`, `instLocallyCompactSpacePontryaginDual`, `PontryaginDual.map_apply`, `PontryaginDual.map_comp`
`instTopologicalSpacePontryaginDual` 📖	CompOp	5 math math: `PontryaginDual.map_one`, `PontryaginDual.map_mul`, `instLocallyCompactSpacePontryaginDual`, `PontryaginDual.map_apply`, `PontryaginDual.map_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallyCompactSpacePontryaginDual` 📖	mathematical	—	`LocallyCompactSpace` `PontryaginDual` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instTopologicalSpacePontryaginDual`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.trans_le` `div_le_self` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.pi_nonneg` `one_le_pow₀` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `one_le_two` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Circle.arg_exp` `neg_lt_of_abs_lt` `covariant_swap_add_of_covariant_add` `LT.lt.le` `lt_of_abs_lt` `Circle.exp_arg` `ContinuousMonoidHom.locallyCompactSpace_of_hasBasis` `Circle.instIsUniformGroup` `T3Space.toT0Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompletelyNormalSpace.toNormalSpace` `UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity` `EMetric.instIsCountablyGeneratedUniformity` `Circle.instCompactSpace` `pow_succ` `div_div` `lt_div_iff₀'` `two_pos` `NeZero.charZero_one` `RCLike.charZero_rclike` `abs_two` `abs_mul` `two_mul` `Complex.arg_mul` `Circle.coe_ne_zero` `Set.Ioo_subset_Ioc_self` `Set.mem_Ioo` `abs_lt` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `Real.pi_pos` `le_refl` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `le_self_pow₀` `Circle.coe_mul` `Circle.exp_zero` `IsLocalHomeomorph.map_nhds_eq` `isLocalHomeomorph_circleExp` `Filter.HasBasis.map` `Filter.HasBasis.to_hasBasis` `nhds_basis_zero_abs_lt` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Set.mem_setOf_eq` `lt_of_lt_of_le` `div_le_iff₀'` `pow_pos` `div_le_iff₀` `LE.le.trans` `Nat.le_ceil` `div_pos` `IsStrictOrderedRing.toZeroLEOneClass` `le_rfl`

---

← Back to Index