Theorem IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedean

Modification history

2026-04-27 19:30
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(NumberTheory/Height/NumberField): results on heights over the rational numbers (#38183) …
Deleted IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedeanView on Github →
2025-04-10 16:38
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedeanView on Github →
2025-03-27 09:53
Mathlib/Algebra/Order/Ring/IsNonarchimedean.lean
feat(Algebra/Order/Ring/IsNonarchimedean.lean): Nonarchimedean functions and APIs (#21963) …
Added IsNonarchimedean.apply_intCast_le_one_of_isNonarchimedeanView on Github →