NormedValued

📁 Source: ClassFieldTheory/Mathlib/Topology/Algebra/Valued/NormedValued.lean

Statistics

Metric	Count
Definitions toValuativeRel, valuativeRel	2
Theorems of_trivial_norm, norm_lt_one_iff_eq_zero_of_discrete, ball_norm_eq, compatible, isEquiv, isNontrivial, isValuativeTopology, nhds_zero_basis_norm, trivial_or_non_trivial, valuation_ball_eq	10
Total	12

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_trivial_norm 📖	—	—	—	—	—

NormedDivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_lt_one_iff_eq_zero_of_discrete 📖	—	—	—	—	—

NormedField

Definitions

Name	Category	Theorems
toValuativeRel 📖	CompOp	3 math math: isNontrivial, compatible, isEquiv
valuativeRel 📖	CompOp	1 math math: isValuativeTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_norm_eq 📖	—	—	—	—	—
compatible 📖	mathematical	—	toValuativeRel	—	—
isEquiv 📖	mathematical	—	toValuativeRel	—	compatible
isNontrivial 📖	mathematical	—	toValuativeRel	—	isEquiv
isValuativeTopology 📖	mathematical	—	valuativeRel	—	compatible ValuativeRel.unitsMap_valuation_surjective
nhds_zero_basis_norm 📖	—	—	—	—	trivial_or_non_trivial
trivial_or_non_trivial 📖	—	—	—	—	—
valuation_ball_eq 📖	mathematical	—	Valuation.ball	—	—

---

← Back to Index