Theorem IsNonarchimedean.apply_sum_le

Modification history

2026-04-27 19:30

Mathlib/NumberTheory/Height/MvPolynomial.lean

feat(NumberTheory/Height/NumberField): results on heights over the rational numbers (#38183) …

Modified IsNonarchimedean.apply_sum_le View on Github →

2026-03-06 11:44

Mathlib/NumberTheory/Height/MvPolynomial.lean

feat(NumberTheory/Height/MvPolynomial): new file (#35925) …

Added IsNonarchimedean.apply_sum_le View on Github →