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	WithZero Multiplicative Preorder.toLT WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Monoid.toPow MonoidWithZero.toMonoid WithZero.instMonoidWithZero Multiplicative.monoid Int.instAddMonoid 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 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace toUniformSpace WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.HasBasis.tendsto_right_iff hasBasis_nhds_zero map_pow MonoidWithZeroHomClass.toMonoidHomClass instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat exists_pow_lt₀ Valuation.restrict_lt_iff_lt_embedding LT.lt.trans_le' pow_le_pow_right_of_le_one' IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid LT.lt.le

---

← Back to Index