Commit 2023-06-21 07:53 c4d449e2

View on Github →

feat: port NumberTheory.FunctionField (#5332)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/FunctionField.lean

added def FunctionField.FqtInfty

added theorem FunctionField.InftyValuation.map_add_le_max'

added theorem FunctionField.InftyValuation.map_mul'

added theorem FunctionField.InftyValuation.map_one'

added theorem FunctionField.InftyValuation.map_zero'

added theorem FunctionField.inftyValuation.C

added theorem FunctionField.inftyValuation.X

added theorem FunctionField.inftyValuation.polynomial

added def FunctionField.inftyValuation

added def FunctionField.inftyValuationDef

added theorem FunctionField.inftyValuation_apply

added theorem FunctionField.inftyValuation_of_nonzero

added theorem FunctionField.inftyValuedFqt.def

added def FunctionField.inftyValuedFqt

added theorem FunctionField.ringOfIntegers.algebraMap_injective

added theorem FunctionField.ringOfIntegers.not_isField

added def FunctionField.ringOfIntegers

added theorem FunctionField.valuedFqtInfty.def

added theorem algebraMap_injective

added theorem functionField_iff