Zulip Chat Archive

Stream: triage

Topic: PR !4#27972: chore: make `Valuation.Completion` a `def` a...

Random Issue Bot (Aug 19 2025 at 14:07):

Today I chose PR #27972 for discussion!

chore: make Valuation.Completion a def and refactor more of AdicValuation.lean
Created by @Salvatore Mercuri (@smmercuri) on 2025-08-05
Labels: WIP, t-number-theory, t-algebra

Is this PR still relevant? Any recent updates? Anyone making progress?

Last updated: Dec 20 2025 at 21:32 UTC