Theorem IsNonarchimedean.apply_intCast_le_one

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) …
Modified IsNonarchimedean.apply_intCast_le_oneView on Github →
2026-04-27 19:30
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(NumberTheory/Height/NumberField): results on heights over the rational numbers (#38183) …
Added IsNonarchimedean.apply_intCast_le_oneView on Github →