Commit 2025-12-17 05:35 5171a5d1

View on Github →

feat: lemmas about the House of an algebraic number (#32218) Lemmas missing for the formalisation of the proof of the Gelfond–Schneider theorem

Estimated changes

Modified Mathlib/NumberTheory/NumberField/House.lean

added theorem NumberField.exists_conjugate_one_le_norm

added theorem NumberField.house_add_le

added theorem NumberField.house_nat_mul

added theorem NumberField.house_pow_le

added theorem NumberField.house_prod_le

added theorem NumberField.norm_embedding_le_house

added theorem NumberField.norm_norm_le_norm_mul_house_pow

added theorem NumberField.one_le_house_of_isIntegral