Commit 2026-04-11 14:19 fd68cd66

View on Github →

chore(FunctionField): rename vars when constant field is not nec. finite (#37894) Asked by @MichaelStollBayreuth here. I've also slightly adjusted the doc to reflect this. I used the notation which I know from Rosen - Number Theory in Function Field.

Estimated changes

Modified Mathlib/NumberTheory/FunctionField.lean

modified def FunctionField.FqtInfty

modified theorem FunctionField.InftyValuation.map_add_le_max'

modified theorem FunctionField.InftyValuation.map_mul'

modified theorem FunctionField.InftyValuation.map_one'

modified theorem FunctionField.InftyValuation.map_zero'

modified theorem FunctionField.algebraMap_injective

modified theorem FunctionField.inftyValuation.C

modified theorem FunctionField.inftyValuation.X

modified theorem FunctionField.inftyValuation.X_inv

modified theorem FunctionField.inftyValuation.X_zpow

modified theorem FunctionField.inftyValuation.polynomial

modified def FunctionField.inftyValuation

modified def FunctionField.inftyValuationDef

modified theorem FunctionField.inftyValuation_apply

modified theorem FunctionField.inftyValuation_of_nonzero

modified theorem FunctionField.inftyValuedFqt.def

modified def FunctionField.inftyValuedFqt

modified theorem FunctionField.ringOfIntegers.algebraMap_injective

modified theorem FunctionField.ringOfIntegers.not_isField

modified def FunctionField.ringOfIntegers

modified theorem FunctionField.valuedFqtInfty.def

modified theorem functionField_iff