Theorem Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_one

Modification history

2026-04-27 19:30
Mathlib/NumberTheory/Height/NumberField.lean
feat(NumberTheory/Height/NumberField): results on heights over the rational numbers (#38183) …
Added Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_oneView on Github →