WellApproximable

📁 Source: Mathlib/NumberTheory/WellApproximable.lean

Statistics

Metric	Count
Definitions addWellApproximable, approxAddOrderOf, approxOrderOf, wellApproximable	4
Theorems addWellApproximable_ae_empty_or_univ, exists_norm_nsmul_le, exists_norm_nsmul_le, mem_addWellApproximable_iff, mem_approxAddOrderOf_iff, image_nsmul_subset, image_nsmul_subset_of_coprime, vadd_eq_of_mul_dvd, vadd_subset_of_coprime, image_pow_subset, image_pow_subset_of_coprime, smul_eq_of_mul_dvd, smul_subset_of_coprime, mem_add_wellApproximable_iff, mem_approxOrderOf_iff, mem_approx_add_orderOf_iff, mem_wellApproximable_iff	17
Total	21

AddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addWellApproximable_ae_empty_or_univ 📖	mathematical	Filter.Tendsto Real Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	Filter.Eventually AddCircle Real.instAddCommGroup addWellApproximable SeminormedAddCommGroup.toSeminormedAddGroup QuotientAddGroup.instSeminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume	—	MeasureTheory.Measure.instOuterMeasureClass addOrderOf_div_of_gcd_eq_one Real.instIsStrictOrderedRing Nat.Prime.pos gcd_one_left Monotone.tendsto_atTop_atTop Nat.exists_infinite_primes MeasurableSet.measurableSet_blimsup IsOpen.measurableSet BorelSpace.opensMeasurable QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples Metric.isOpen_thickening MeasurableSet.nullMeasurableSet sq MeasureTheory.union_ae_eq_right_of_ae_eq_empty Filter.EventuallyEq.trans LE.le.trans sSupHom.apply_blimsup_le Filter.mono_blimsup Nat.Prime.coprime_iff_not_dvd approxAddOrderOf.image_nsmul_subset_of_coprime Ergodic.ae_empty_or_univ_of_image_ae_le isFiniteMeasure ergodic_nsmul Nat.Prime.one_lt Filter.EventuallyLE.congr HasSubset.Subset.eventuallyLE Filter.EventuallyEq.rfl blimsup_thickening_mul_ae_eq QuotientAddGroup.instSecondCountableTopology IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts instWeaklyLocallyCompactSpaceOfLocallyCompactSpace QuotientAddGroup.instLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts instIsAddHaarMeasureRealVolume instIsUnifLocDoublingMeasureRealVolume Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial mul_dvd_mul_left add_comm sSupHom.setImage_toFun Set.image_comp Set.monotone_image approxAddOrderOf.image_nsmul_subset mul_comm approxAddOrderOf.vadd_subset_of_coprime ergodic_nsmul_add Filter.eventuallyEq_empty Filter.eventuallyEq_univ OrderIso.apply_blimsup Filter.blimsup_congr Filter.Eventually.of_forall approxAddOrderOf.vadd_eq_of_mul_dvd MeasureTheory.MeasurePreserving.quasiMeasurePreserving MeasureTheory.measurePreserving_vadd MeasurableVAdd.toMeasurableConstVAdd measurableVAdd_of_add ContinuousAdd.measurableAdd IsTopologicalAddGroup.toContinuousAdd QuotientAddGroup.instIsTopologicalAddGroup MeasureTheory.Measure.IsAddLeftInvariant.vaddInvariantMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq MeasureTheory.ae_eq_trans Filter.EventuallyEq.refl Filter.EventuallyEq.symm ae_empty_or_univ_of_forall_vadd_ae_eq_self Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_or_eq
exists_norm_nsmul_le 📖	mathematical	—	Set Set.instMembership Set.Icc Nat.instPreorder Real Real.instLE Norm.norm AddCircle Real.instAddCommGroup QuotientAddGroup.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instNormedAddCommGroupReal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast	—	NormedAddCommGroup.exists_norm_nsmul_le compactSpace ConnectedSpace.toPreconnectedSpace PathConnectedSpace.connectedSpace pathConnectedSpace QuotientAddGroup.borelSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable Real.instCompleteSpace EMetric.instIsCountablyGeneratedUniformity T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace instIsTopologicalAddGroupReal Real.borelSpace AddSubgroup.normal_of_comm AddSubgroup.isClosed_of_discrete TopologicalSpace.t2Space_of_metrizableSpace Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples instIsAddHaarMeasureRealVolume Nat.instAtLeastTwoHAddOfNat measure_univ volume_closedBall ENNReal.ofReal_nsmul mul_div_cancel₀ two_ne_zero CharZero.NeZero.two RCLike.charZero_rclike min_eq_right div_le_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le Fact.out Nat.cast_add Nat.cast_one covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Real.instIsOrderedRing nsmul_eq_mul Nat.cast_ne_zero le_refl

NormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_norm_nsmul_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.univ AddMonoid.toNatSMul ESeminormedAddMonoid.toAddMonoid ENNReal.instTopologicalSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instENormedAddCommMonoidENNReal Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid toAddCommGroup Real DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Set.instMembership Set.Icc Nat.instPreorder Real.instLE Norm.norm toNorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat Metric.isClosed_closedBall LT.lt.ne' IsClosed.measure_eq_univ_iff_eq MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure BorelSpace.opensMeasurable MeasureTheory.CompactSpace.isFiniteMeasure MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts isClosed_iUnion_of_finite Finite.of_fintype le_antisymm MeasureTheory.OuterMeasure.mono Set.subset_univ MeasureTheory.measure_iUnion SetCoe.countable instCountableNat measurableSet_closedBall tsum_fintype SummationFilter.instLeAtTopUnconditional Finset.sum_congr MeasureTheory.Measure.addHaar_closedBall_center Finset.sum_const Fintype.card_Icc Nat.card_Icc tsub_zero Nat.instOrderedSub LT.lt.not_ge IsOpen.measure_pos isOpen_univ Set.univ_nonempty AddTorsor.nonempty LE.le.trans Metric.closedBall_eq_empty not_le MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass nsmul_zero Metric.nonempty_closedBall Nat.instCanonicallyOrderedAdd subsingleton_of_disjoint_isClosed_iUnion_eq_univ exists_lt_mem_inter_of_not_pairwise_disjoint le_tsub_of_add_le_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_self_add sub_nsmul Subtype.coe_le_coe LT.lt.le sub_eq_add_neg dist_eq_norm dist_triangle le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Metric.mem_closedBall Metric.mem_closedBall'

UnitAddCircle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_addWellApproximable_iff 📖	mathematical	—	UnitAddCircle Set Set.instMembership addWellApproximable SeminormedAddCommGroup.toSeminormedAddGroup QuotientAddGroup.instSeminormedAddCommGroup Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instAddCommGroup Real.instOne Set.Infinite setOf GCDMonoid.gcd Nat.instCommMonoidWithZero instGCDMonoidNat Real.instLT Norm.norm QuotientAddGroup.instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast	—	AddSubgroup.normal_of_comm Filter.cofinite.blimsup_set_eq Set.ext mem_approxAddOrderOf_iff pos_of_gt Nat.instCanonicallyOrderedAdd
mem_approxAddOrderOf_iff 📖	mathematical	—	UnitAddCircle Set Set.instMembership approxAddOrderOf SeminormedAddCommGroup.toSeminormedAddGroup QuotientAddGroup.instSeminormedAddCommGroup Real NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instAddCommGroup Real.instOne GCDMonoid.gcd Nat.instCommMonoidWithZero instGCDMonoidNat Real.instLT Norm.norm QuotientAddGroup.instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddSubgroup.normal_of_comm DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast	—	AddSubgroup.normal_of_comm AddCircle.addOrderOf_eq_pos_iff Real.instIsStrictOrderedRing ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mul_one dist_eq_norm

(root)

Definitions

Name	Category	Theorems
addWellApproximable 📖	CompOp	3 math math: mem_add_wellApproximable_iff, AddCircle.addWellApproximable_ae_empty_or_univ, UnitAddCircle.mem_addWellApproximable_iff
approxAddOrderOf 📖	CompOp	7 math math: approxAddOrderOf.vadd_eq_of_mul_dvd, mem_approx_add_orderOf_iff, mem_add_wellApproximable_iff, UnitAddCircle.mem_approxAddOrderOf_iff, approxAddOrderOf.image_nsmul_subset, approxAddOrderOf.image_nsmul_subset_of_coprime, approxAddOrderOf.vadd_subset_of_coprime
approxOrderOf 📖	CompOp	6 math math: mem_approxOrderOf_iff, approxOrderOf.image_pow_subset_of_coprime, approxOrderOf.smul_subset_of_coprime, mem_wellApproximable_iff, approxOrderOf.image_pow_subset, approxOrderOf.smul_eq_of_mul_dvd
wellApproximable 📖	CompOp	1 math math: mem_wellApproximable_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_add_wellApproximable_iff 📖	mathematical	—	Set Set.instMembership addWellApproximable Filter.blimsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra approxAddOrderOf Filter.atTop Nat.instPreorder	—	—
mem_approxOrderOf_iff 📖	mathematical	—	Set Set.instMembership approxOrderOf orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup Metric.ball SeminormedGroup.toPseudoMetricSpace	—	Metric.thickening_eq_biUnion_ball
mem_approx_add_orderOf_iff 📖	mathematical	—	Set Set.instMembership approxAddOrderOf addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup Metric.ball SeminormedAddGroup.toPseudoMetricSpace	—	Metric.thickening_eq_biUnion_ball Set.mem_iUnion₂
mem_wellApproximable_iff 📖	mathematical	—	Set Set.instMembership wellApproximable Filter.blimsup CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra approxOrderOf Filter.atTop Nat.instPreorder	—	—

approxAddOrderOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_nsmul_subset 📖	mathematical	—	Set Set.instHasSubset Set.image AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup approxAddOrderOf Real Real.instMul Real.instNatCast	—	mem_approx_add_orderOf_iff Set.mem_setOf_eq addOrderOf_nsmul' LT.lt.ne' Metric.ball_subset_thickening nsmul_eq_mul nsmul_mem_ball
image_nsmul_subset_of_coprime 📖	mathematical	—	Set Set.instHasSubset Set.image AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup approxAddOrderOf Real Real.instMul Real.instNatCast	—	mem_approx_add_orderOf_iff Nat.Coprime.addOrderOf_nsmul Metric.ball_subset_thickening nsmul_eq_mul nsmul_mem_ball
vadd_eq_of_mul_dvd 📖	mathematical	Monoid.toNatPow Nat.instMonoid addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction approxAddOrderOf	—	Metric.thickening_eq_biUnion_ball Set.image_iUnion₂ Set.iUnion_congr_Prop vadd_ball'' AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd AddCommute.all addOrderOf_pos_iff dvd_trans mul_dvd_mul_right sq Set.mem_setOf_eq addOrderOf_neg neg_add_rev neg_neg add_comm add_neg_cancel_left Set.iUnion_coe_set Function.Surjective.iUnion_comp
vadd_subset_of_coprime 📖	mathematical	addOrderOf SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	Set Set.instHasSubset HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddMonoid.toAddAction approxAddOrderOf	—	Metric.thickening_eq_biUnion_ball Set.image_iUnion₂ Set.iUnion_congr_Prop vadd_ball'' Set.iUnion₂_subset_iff Set.mem_iUnion AddCommute.addOrderOf_add_eq_mul_addOrderOf_of_coprime AddCommute.all

approxOrderOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_pow_subset 📖	mathematical	—	Set Set.instHasSubset Set.image Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup approxOrderOf Real Real.instMul Real.instNatCast	—	mem_approxOrderOf_iff Set.mem_setOf_eq orderOf_pow' LT.lt.ne' Metric.ball_subset_thickening nsmul_eq_mul pow_mem_ball
image_pow_subset_of_coprime 📖	mathematical	—	Set Set.instHasSubset Set.image Monoid.toNatPow DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup approxOrderOf Real Real.instMul Real.instNatCast	—	mem_approxOrderOf_iff Nat.Coprime.orderOf_pow Metric.ball_subset_thickening nsmul_eq_mul pow_mem_ball
smul_eq_of_mul_dvd 📖	mathematical	Monoid.toNatPow Nat.instMonoid orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction approxOrderOf	—	Metric.thickening_eq_biUnion_ball Set.image_iUnion₂ Set.iUnion_congr_Prop smul_ball'' Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd Commute.all orderOf_pos_iff dvd_trans mul_dvd_mul_right sq Set.mem_setOf_eq orderOf_inv mul_inv_rev inv_inv mul_comm mul_inv_cancel_left Set.iUnion_coe_set Function.Surjective.iUnion_comp
smul_subset_of_coprime 📖	mathematical	orderOf DivInvMonoid.toMonoid Group.toDivInvMonoid SeminormedGroup.toGroup SeminormedCommGroup.toSeminormedGroup	Set Set.instHasSubset Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Monoid.toMulAction approxOrderOf	—	Metric.thickening_eq_biUnion_ball Set.image_iUnion₂ Set.iUnion_congr_Prop smul_ball'' Set.iUnion₂_subset_iff Commute.orderOf_mul_eq_mul_orderOf_of_coprime Commute.all

---

← Back to Index