Commit 2022-11-19 14:36 bc5c9b40

View on Github →

feat(ring_theory/ideal): define absolute ideal norm (#17203) This PR defines the absolute ideal norm ideal.abs_norm on a number ring (specifically, a Dedekind domain that is a finite, free extension of ℤ) as the finite cardinality of the quotient ideal (and zero if the cardinality is infinite).

Estimated changes

Modified src/algebra/associated.lean

added theorem prime_pow_succ_dvd_mul

Modified src/ring_theory/ideal/norm.lean

added theorem card_quot_mul

added theorem card_quot_mul_of_coprime

added theorem card_quot_pow_of_prime

added theorem ideal.exists_mul_add_mem_pow_succ

added theorem ideal.mem_prime_of_mul_mem_pow

added theorem ideal.mul_add_mem_pow_succ_inj

added theorem ideal.mul_add_mem_pow_succ_unique