Def RatFunc.CompletionAtInfty

Modification history

2026-04-14 14:26

Mathlib/FieldTheory/RatFunc/Valuation.lean

chore(FunctionField): move `inftyValuation` and `FqtInfty` to `RatFunc` namespace (#38030) …

Added RatFunc.CompletionAtInfty View on Github →