ValuativeRel

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

Statistics

Metric	Count
Definitions instValuedValueGroupWithZeroOfIsUniformAddGroup, ValuativeRel, «term𝒪[_]», «term𝓀[_]», «term𝓂[_]»	5
Theorems continuous_valuation, of_zero, v_eq_valuation	3
Total	8

IsValuativeTopology

Definitions

Name	Category	Theorems
instValuedValueGroupWithZeroOfIsUniformAddGroup 📖	CompOp	2 math math: v_eq_valuation, IsNonarchimedeanLocalField.instCompatibleValueGroupWithZeroV

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_valuation 📖	mathematical	—	Continuous ValuativeRel.ValueGroupWithZero WithZeroTopology.topologicalSpace ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation	—	ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass MonoidWithZeroHom.monoidWithZeroHomClass Filter.HasBasis.tendsto_iff Valuation.hasBasis_nhds ValuativeRel.instCompatibleValueGroupWithZeroValuation WithZeroTopology.hasBasis_nhds_zero OrderMonoidIso.instMulEquivClass Valuation.map_sub_of_right_eq_zero WithZeroTopology.hasBasis_nhds_of_ne_zero ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀ Valuation.map_eq_of_sub_lt
of_zero 📖	mathematical	Set Filter Filter.instMembership nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units ValuativeRel.ValueGroupWithZero MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero Set.instHasSubset setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ValuativeRel.instLinearOrderValueGroupWithZero DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero CommRing.toRing Valuation.instFunLike ValuativeRel.valuation Units.val	IsValuativeTopology	—	vadd_mem_nhds_vadd_iff neg_add_cancel Set.image_congr Set.image_add_left neg_neg
v_eq_valuation 📖	mathematical	—	Valued.v CommRing.toRing ValuativeRel.ValueGroupWithZero ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero instValuedValueGroupWithZeroOfIsUniformAddGroup ValuativeRel.valuation	—	—

ValuativeRel

Definitions

Name	Category	Theorems
«term𝒪[_]» 📖	CompOp	—
«term𝓀[_]» 📖	CompOp	—
«term𝓂[_]» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ValuativeRel 📖	CompData	—

---

← Back to Index