Documentation Verification Report

DenseSubgroup

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

Statistics

Metric	Count
Definitions	0
Theorems `denseRange_zsmul_coe_iff`, `denseRange_zsmul_iff`, `dense_addSubgroup_iff_ne_zmultiples`, `dense_addSubgroupClosure_pair_iff`	4
Total	4

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denseRange_zsmul_coe_iff` 📖	mathematical	—	`DenseRange` `HasQuotient.Quotient` `Real` `AddSubgroup` `AddCommGroup.toAddGroup` `Real.instAddCommGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `AddSubgroup.zmultiples` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `Irrational` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`AddSubgroup.normal_of_comm` `dense_addSubgroupClosure_pair_iff` `DenseRange.eq_1` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `QuotientAddGroup.coe_mk'` `AddSubgroup.coe_zmultiples` `AddSubgroup.coe_comap` `AddMonoidHom.map_zmultiples` `AddSubgroup.comap_map_eq` `QuotientAddGroup.ker_mk'` `AddSubgroup.zmultiples_eq_closure` `AddSubgroup.closure_union` `Set.insert_eq`
`denseRange_zsmul_iff` 📖	mathematical	—	`DenseRange` `AddCircle` `Real` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `addOrderOf` `SubNegMonoid.toAddMonoid`	—	`AddSubgroup.normal_of_comm` `QuotientAddGroup.mk_surjective` `Real.instIsStrictOrderedRing`
`dense_addSubgroup_iff_ne_zmultiples` 📖	mathematical	—	`Dense` `AddCircle` `Real` `Real.instAddCommGroup` `QuotientAddGroup.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `AddCommGroup.toAddGroup` `AddSubgroup.zmultiples` `SetLike.coe` `AddSubgroup` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `AddSubgroup.instSetLike`	—	`AddSubgroup.normal_of_comm` `denseRange_zsmul_iff` `DenseRange.eq_1` `AddSubgroup.coe_zmultiples` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `xor_iff_not_iff'` `AddSubgroup.dense_xor'_cyclic` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `Real.instArchimedean` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddSubgroup.coe_comap` `QuotientAddGroup.coe_mk'` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `AddMonoidHom.map_zmultiples` `AddSubgroup.map_comap_eq_self_of_surjective` `Quot.mk_surjective` `Iff.not`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_addSubgroupClosure_pair_iff` 📖	mathematical	—	`Dense` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SetLike.coe` `AddSubgroup` `Real.instAddGroup` `AddSubgroup.instSetLike` `AddSubgroup.closure` `Set` `Set.instInsert` `Set.instSingletonSet` `Irrational` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`eq_or_ne` `Set.pair_comm` `AddSubgroup.closure_insert_zero` `div_zero` `not_denseRange_zsmul` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Dense.mono` `AddSubgroup.coe_zmultiples` `SetLike.coe_subset_coe` `instIsConcreteLE` `AddSubgroup.closure_le` `Set.pair_subset_iff` `zsmul_eq_mul` `mul_div_left_comm` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Int.cast_natCast` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₁` `AddSubgroup.dense_or_cyclic` `Real.instArchimedean` `AddSubgroup.zmultiples_eq_closure` `AddSubgroup.subset_closure` `mul_div_mul_right` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE`

---

← Back to Index