Commit 2024-10-24 10:44 a5a07115

View on Github →

feat(RingTheory/Ideal/Norm): Generalize Ideal.finite_setOf_absNorm_eq and add Ideal.finite_setOf_absNorm_le (#18132) Also:

prove some results about the norm of nonZeroDivisors ideals
golf the proof of Dirichlet unit theorem using the generalization
clean up the import of RingTheory.Ideal.Norm This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

deleted theorem NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero

Modified Mathlib/RingTheory/Ideal/Norm.lean

added theorem Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors

modified theorem Ideal.absNorm_ne_zero_of_nonZeroDivisors

added theorem Ideal.absNorm_pos_iff_mem_nonZeroDivisors

added theorem Ideal.absNorm_pos_of_nonZeroDivisors

added theorem Ideal.card_norm_le_eq_card_norm_le_add_one

modified theorem Ideal.finite_setOf_absNorm_eq

added theorem Ideal.finite_setOf_absNorm_le