Commit 2026-03-12 15:10 8f787c67
View on Github →feat(NumberTheory/FunctionField): add instances on FqtInfty (#35720)
This PR proves the relevant instances on FqtInfty by locally replacing the existing valued instance RatFunc.valuedRatFunc coming from the ideal X with the required UniformSpace instance coming from the valuation at infinity and then deriving the relevant instances.