Theorem IsNonarchimedean.nsmul_le_of_pos

Modification history

2026-08-16 13:11
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
chore(Algebra/Order/Ring/IsNonarchimedean): remove FunLike hypotheses and generalize statements (#42408) …
Added IsNonarchimedean.nsmul_le_of_posView on Github →