WithZeroMulInt

📁 Source: Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_pow_lt_of_le_exp_neg_one, tendsto_zero_pow_of_le_exp_neg_one, tendsto_zero_pow_of_v_lt_one	3
Total	3

Valued

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pow_lt_of_le_exp_neg_one 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Valuation.instFunLike v WithZero.exp	Preorder.toLT Monoid.toNatPow MonoidWithZero.toMonoid WithZero.instMonoidWithZero Multiplicative.monoid Int.instAddMonoid Units.val	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid exists_pow_lt₀ WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt LE.le.trans_lt WithZero.exp_zero WithZero.exp_lt_exp Int.instZeroLEOneClass
tendsto_zero_pow_of_le_exp_neg_one 📖	mathematical	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Valuation.instFunLike v WithZero.exp	Filter.Tendsto Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid tendsto_zero_pow_of_v_lt_one WithZero.instMulArchimedean Multiplicative.instMulArchimedean instArchimedeanInt LE.le.trans_lt WithZero.exp_zero WithZero.exp_lt_exp Int.instZeroLEOneClass
tendsto_zero_pow_of_v_lt_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike v InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	Filter.Tendsto Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Filter.HasBasis.tendsto_right_iff hasBasis_nhds_zero map_pow MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat exists_pow_lt₀ LT.lt.trans_le' pow_le_pow_right_of_le_one' IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid LT.lt.le

---

← Back to Index