Def WithVal

Modification history

2026-03-02 10:51

Mathlib/Topology/Algebra/Valued/WithVal.lean

refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …

Deleted WithVal View on Github →

2025-04-16 22:42

Mathlib/Topology/Algebra/Valued/WithVal.lean

chore(Topology.Algebra.Valued.WithVal): clean up typeclass assumptions (#24125) …

Modified WithVal View on Github →

2025-03-01 13:14

Mathlib/Topology/Algebra/Valued/WithVal.lean

feat: `WithVal` type synonym and refactor of `HeightOneSpectrum.adicCompletion` (#22055) …

Added WithVal View on Github →