Commit 2025-08-14 19:32 a538d753

View on Github →

refactor(FunctionField): use exp instead of ofAdd (#28283) Make the valuation at infinity in FunctionField use the notation WithZero.exp instead of Multiplicative.ofAdd. I have also tagged many of the exp lemmas with simp making most basic results provable with simp. I have left the proofs with rw in this file as this is faster, but having the option to close similar goals with simp is nice for further development.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Int.lean

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

modified theorem WithZero.exp_add

modified theorem WithZero.exp_neg

modified theorem WithZero.exp_nsmul

modified theorem WithZero.exp_sub

modified theorem WithZero.exp_zsmul

Modified Mathlib/NumberTheory/FunctionField.lean

modified theorem FunctionField.inftyValuation.X

added theorem FunctionField.inftyValuation.X_inv

added theorem FunctionField.inftyValuation.X_zpow

modified theorem FunctionField.valuedFqtInfty.def

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/ValuativeRel.lean