Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 10:12 04274301

View on Github →

feat(number_theory/function_field): add completion with respect to place at infinity (#12715)

Estimated changes

Modified src/number_theory/function_field.lean

added def function_field.Fqt_infty

added theorem function_field.infty_valued_Fqt.completable_top_field

added theorem function_field.infty_valued_Fqt.def

added theorem function_field.infty_valued_Fqt.separated_space

added theorem function_field.infty_valued_Fqt.topological_division_ring

added def function_field.infty_valued_Fqt.topological_space

added theorem function_field.infty_valued_Fqt.uniform_add_group

added def function_field.infty_valued_Fqt.uniform_space

added def function_field.infty_valued_Fqt

added theorem function_field.valued_Fqt_infty.def