Theorem IsNonarchimedean.iSup_abv_linearMap_apply_le

Modification history

2026-03-06 11:44
Mathlib/NumberTheory/Height/MvPolynomial.lean
feat(NumberTheory/Height/MvPolynomial): new file (#35925) …
Added IsNonarchimedean.iSup_abv_linearMap_apply_leView on Github →