Structure AbsoluteValue.Completion

Modification history

2026-10-30 13:18

Mathlib/Analysis/Normed/Field/WithAbs.lean

refactor: make `AbsoluteValue.Completion` a one-field structure (#45407) …

Added AbsoluteValue.Completion View on Github →