Def AbsoluteValue.Completion.equivAux

Modification history

2026-11-10 13:06

Mathlib/Analysis/Normed/Field/WithAbs.lean

refactor: make `InfinitePlace.Completion` an `abbrev` (#45508) …

Added AbsoluteValue.Completion.equivAux View on Github →