ValuativeRel
📁 Source: ClassFieldTheory/Mathlib/Topology/Algebra/Valued/ValuativeRel.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 4 | |
| Total | 4 |
(root)
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
le_valuation_irreducible_of_lt_one 📖 | — | — | — | — | Valuation.Integers.associated_iff_eq |
valuation_eq_one_iff 📖 | — | — | — | — | valuation_units_integer_eq_one |
valuation_map_irreducible_lt_one 📖 | — | — | — | — | — |
valuation_units_integer_eq_one 📖 | — | — | — | — | — |
---