Documentation Verification Report

Real

📁 Source: Mathlib/Topology/Instances/AddCircle/Real.lean

Statistics

Metric	Count
Definitions `UnitAddCircle`, `toAddCircle`	2
Theorems `compactSpace`, `instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples`, `pathConnectedSpace`, `toAddCircle_apply`, `toAddCircle_eq_zero`, `toAddCircle_inj`, `toAddCircle_injective`, `toAddCircle_intCast`, `toAddCircle_natCast`	9
Total	11

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace` 📖	mathematical	—	`CompactSpace` `AddCircle` `Real` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples`	—	`isCompact_univ_iff` `coe_image_Icc_eq` `Real.instIsOrderedAddMonoid` `Real.instArchimedean` `IsCompact.image` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `continuous_mk'`
`instProperlyDiscontinuousVAddSubtypeAddOppositeRealMemAddSubgroupOpZmultiples` 📖	mathematical	—	`ProperlyDiscontinuousVAdd` `AddOpposite` `Real` `AddSubgroup` `AddOpposite.instAddGroup` `Real.instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.op` `AddSubgroup.zmultiples` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddSubgroup.instVAdd`	—	`AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite` `instIsTopologicalAddGroupReal` `AddSubgroup.tendsto_zmultiples_subtype_cofinite`
`pathConnectedSpace` 📖	mathematical	—	`PathConnectedSpace` `AddCircle` `Real` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples`	—	`Quotient.instPathConnectedSpace` `Real.instPathConnectedSpace`

ZMod

Definitions

Name	Category	Theorems
`toAddCircle` 📖	CompOp	12 math math: `LFunction_stdAddChar_eq_expZeta`, `completedLFunction_def_even`, `LFunction_def_odd`, `toAddCircle_inj`, `completedLFunction_def_odd`, `toAddCircle_natCast`, `LFunction_def_even`, `toAddCircle_intCast`, `toAddCircle_apply`, `toAddCircle_injective`, `toAddCircle_eq_zero`, `LFunction_dft`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAddCircle_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ZMod` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `val`	—	`AddSubgroup.normal_of_comm` `toAddCircle_natCast` `natCast_zmod_val`
`toAddCircle_eq_zero` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ZMod` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`map_eq_zero_iff` `AddSubgroup.normal_of_comm` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `toAddCircle_injective`
`toAddCircle_inj` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ZMod` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `toAddCircle_injective`
`toAddCircle_injective` 📖	mathematical	—	`ZMod` `UnitAddCircle` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle`	—	`AddSubgroup.normal_of_comm` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `val_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `div_left_inj'` `LT.lt.ne'` `AddCircle.coe_eq_coe_iff_of_mem_Ico` `Real.instIsOrderedAddMonoid` `ZeroLEOneClass.factZeroLtOne` `Real.instZeroLEOneClass` `NeZero.charZero_one` `Real.instArchimedean` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `zero_add` `div_lt_one` `val_lt` `toAddCircle_apply`
`toAddCircle_intCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ZMod` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle` `AddGroupWithOne.toIntCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast` `Real.instNatCast`	—	`AddSubgroup.normal_of_comm` `lift_coe`
`toAddCircle_natCast` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ZMod` `UnitAddCircle` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `Real` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `AddSubgroup.zmultiples` `Real.instOne` `AddSubgroup.normal_of_comm` `AddMonoidHom.instFunLike` `toAddCircle` `AddMonoidWithOne.toNatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`AddSubgroup.normal_of_comm` `Int.cast_natCast` `toAddCircle_intCast`

(root)

Definitions

Name	Category	Theorems
`UnitAddCircle` 📖	CompOp	81 math math: `HurwitzZeta.isBigO_atTop_evenKernel_sub`, `HurwitzZeta.expZeta_zero`, `UnitAddTorus.coe_mFourierBasis`, `UnitAddCircle.lintegral_preimage`, `ZMod.LFunction_stdAddChar_eq_expZeta`, `UnitAddCircle.intervalIntegral_preimage`, `UnitAddTorus.mFourierSubalgebra_coe`, `UnitAddTorus.mFourierSubalgebra_closure_eq_top`, `HurwitzZeta.hurwitzZetaEven_zero`, `ZMod.completedLFunction_def_even`, `fourierCoeff_bernoulli_eq`, `ZMod.LFunction_def_odd`, `UnitAddTorus.mFourierCoeff_toLp`, `HurwitzZeta.completedSinZeta_neg`, `HurwitzZeta.evenKernel_eq_cosKernel_of_zero`, `HurwitzZeta.hurwitzZetaEven_apply_zero`, `HurwitzZeta.expZeta_one_sub`, `ZMod.toAddCircle_inj`, `ZMod.completedLFunction_def_odd`, `HurwitzZeta.sinKernel_neg`, `UnitAddTorus.mFourier_add`, `UnitAddTorus.mFourier_zero`, `UnitAddCircle.measure_univ`, `HurwitzZeta.hurwitzEvenFEPair_zero_symm`, `UnitAddTorus.coeFn_mFourierLp`, `UnitAddTorus.mFourier_neg`, `HurwitzZeta.cosZeta_eq`, `periodizedBernoulli.continuous`, `HurwitzZeta.completedHurwitzZetaEven_eq`, `UnitAddTorus.mFourier_norm`, `HurwitzZeta.completedCosZeta₀_neg`, `UnitAddTorus.orthonormal_mFourier`, `ZMod.toAddCircle_natCast`, `HurwitzZeta.sinKernel_zero`, `HurwitzZeta.completedCosZeta₀_zero`, `HurwitzZeta.oddKernel_zero`, `UnitAddTorus.instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp`, `UnitAddTorus.hasSum_mFourier_series_L2`, `UnitAddCircle.mem_approxAddOrderOf_iff`, `HurwitzZeta.completedHurwitzZetaOdd_neg`, `ZMod.LFunction_def_even`, `HurwitzZeta.oddKernel_neg`, `HurwitzZeta.evenKernel_neg`, `HurwitzZeta.cosZeta_zero`, `UnitAddCircle.measurePreserving_mk`, `UnitAddTorus.mFourierSubalgebra_separatesPoints`, `HurwitzZeta.completedHurwitzZetaEven_zero`, `ZMod.toAddCircle_intCast`, `ZMod.toAddCircle_apply`, `HurwitzZeta.hurwitzZetaOdd_eq`, `HurwitzZeta.hurwitzZeta_zero`, `HurwitzZeta.hurwitzZeta_one_sub`, `UnitAddTorus.hasSum_prod_mFourierCoeff`, `HurwitzZeta.completedHurwitzZetaEven₀_neg`, `HurwitzZeta.completedHurwitzZetaEven₀_zero`, `ZMod.toAddCircle_injective`, `HurwitzZeta.sinZeta_neg`, `HurwitzZeta.completedCosZeta_eq`, `HurwitzZeta.hurwitzEvenFEPair_neg`, `instIsProbabilityMeasureUnitAddCircleVolume`, `HurwitzZeta.completedHurwitzZetaEven_neg`, `HurwitzZeta.cosKernel_neg`, `UnitAddCircle.mem_addWellApproximable_iff`, `UnitAddTorus.mFourierBasis_repr`, `HurwitzZeta.completedCosZeta_zero`, `HurwitzZeta.completedCosZeta_neg`, `UnitAddTorus.span_mFourier_closure_eq_top`, `HurwitzZeta.cosZeta_neg`, `UnitAddTorus.hasSum_sq_mFourierCoeff`, `UnitAddTorus.mFourier_single`, `HurwitzZeta.hurwitzZetaOdd_neg`, `ZMod.toAddCircle_eq_zero`, `HurwitzZeta.completedHurwitzZetaEven_residue_zero`, `HurwitzZeta.sinZeta_eq`, `instIsAddHaarMeasureUnitAddCircleVolume`, `UnitAddTorus.span_mFourierLp_closure_eq_top`, `ZMod.LFunction_dft`, `UnitAddCircle.integral_preimage`, `HurwitzZeta.hurwitzZetaEven_neg`, `HurwitzZeta.hurwitzZetaEven_eq`, `HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub`

---

← Back to Index