Theorem NumberField.norm_norm_le_norm_mul_house_pow

Modification history

2025-12-17 05:35
Mathlib/NumberTheory/NumberField/House.lean
feat: lemmas about the `House` of an algebraic number (#32218) …
Added NumberField.norm_norm_le_norm_mul_house_powView on Github →