Commit 2023-06-22 06:58 5040af25

View on Github →

feat: port RingTheory.Ideal.Norm (#5311)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Norm.lean

added theorem Ideal.absNorm_apply

added theorem Ideal.absNorm_bot

added theorem Ideal.absNorm_dvd_absNorm_of_le

added theorem Ideal.absNorm_dvd_norm_of_mem

added theorem Ideal.absNorm_eq_one_iff

added theorem Ideal.absNorm_mem

added theorem Ideal.absNorm_ne_zero_iff

added theorem Ideal.absNorm_span_insert

added theorem Ideal.absNorm_span_singleton

added theorem Ideal.absNorm_top

added theorem Ideal.exists_mul_add_mem_pow_succ

added theorem Ideal.finite_setOf_absNorm_eq

added theorem Ideal.irreducible_of_irreducible_absNorm

added theorem Ideal.isPrime_of_irreducible_absNorm

added theorem Ideal.map_relNorm

added theorem Ideal.map_spanNorm

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

added theorem Ideal.natAbs_det_basis_change

added theorem Ideal.natAbs_det_equiv

added theorem Ideal.norm_mem_relNorm

added theorem Ideal.norm_mem_spanNorm

added theorem Ideal.prime_of_irreducible_absNorm_span

added def Ideal.relNorm

added theorem Ideal.relNorm_apply

added theorem Ideal.relNorm_bot

added theorem Ideal.relNorm_eq_bot_iff

added theorem Ideal.relNorm_mono

added theorem Ideal.relNorm_singleton

added theorem Ideal.relNorm_top

added def Ideal.spanNorm

added theorem Ideal.spanNorm_bot

added theorem Ideal.spanNorm_eq

added theorem Ideal.spanNorm_eq_bot_iff

added theorem Ideal.spanNorm_localization

added theorem Ideal.spanNorm_mono

added theorem Ideal.spanNorm_mul

added theorem Ideal.spanNorm_mul_of_bot_or_top

added theorem Ideal.spanNorm_mul_of_field

added theorem Ideal.spanNorm_mul_spanNorm_le

added theorem Ideal.spanNorm_singleton

added theorem Ideal.spanNorm_top

added theorem Ideal.span_singleton_absNorm_le

added theorem Submodule.cardQuot_apply

added theorem Submodule.cardQuot_bot

added theorem Submodule.cardQuot_eq_one_iff

added theorem Submodule.cardQuot_top

added theorem cardQuot_mul

added theorem cardQuot_mul_of_coprime

added theorem cardQuot_pow_of_prime