mathlib

8d2e8871 - feat(number_theory/function_field): add place at infinity (#12245)