Commit 2026-08-16 13:11 6d003152

View on Github →

chore(Algebra/Order/Ring/IsNonarchimedean): remove FunLike hypotheses and generalize statements (#42408) This PR generalizes the IsNonarchimedean API from FunLike maps to arbitrary functions f : α → R, replacing bundled typeclass assumptions with explicit hypotheses.

Estimated changes

Modified Mathlib/Algebra/Order/Hom/Basic.lean

added theorem map_zero_le

Modified Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean

modified theorem IsNonarchimedean.add_eq_left_of_lt

deleted theorem IsNonarchimedean.add_eq_max_of_ne'

modified theorem IsNonarchimedean.add_eq_max_of_ne

modified theorem IsNonarchimedean.add_eq_right_of_lt

modified theorem IsNonarchimedean.add_le

modified theorem IsNonarchimedean.add_pow_le

modified theorem IsNonarchimedean.apply_intCast_le_one

modified theorem IsNonarchimedean.apply_natCast_le_one

modified theorem IsNonarchimedean.apply_sum_eq_of_lt

modified theorem IsNonarchimedean.apply_sum_le_sup

modified theorem IsNonarchimedean.finset_image_add

modified theorem IsNonarchimedean.finset_image_add_of_nonempty

modified theorem IsNonarchimedean.finset_powerset_image_add

modified theorem IsNonarchimedean.multiset_image_add

modified theorem IsNonarchimedean.multiset_image_add_of_nonempty

modified theorem IsNonarchimedean.multiset_powerset_image_add

modified theorem IsNonarchimedean.nmul_le

added theorem IsNonarchimedean.nmul_le_of_pos

modified theorem IsNonarchimedean.nsmul_le

added theorem IsNonarchimedean.nsmul_le_of_pos

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

Modified Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Modified Mathlib/NumberTheory/Height/NumberField.lean

Modified Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

Modified Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean

Modified Mathlib/RingTheory/Polynomial/GaussNorm.lean