Commit 2025-06-14 13:55 50e49dc2

View on Github →

feat(NumberTheory): discriminant is norm of different (#25792)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

added theorem Submodule.toIntSubmodule_toAddSubgroup

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem AddSubgroup.toIntSubmodule_closure

added theorem AddSubmonoid.toNatSubmodule_closure

Created Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

added theorem NumberField.absNorm_differentIdeal

added theorem NumberField.discr_mem_differentIdeal

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem Submodule.restrictScalars_traceDual

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

added def FractionalIdeal.divMod

added theorem FractionalIdeal.divMod_spec

added theorem FractionalIdeal.divMod_zero_left

added theorem FractionalIdeal.divMod_zero_of_not_le

added theorem FractionalIdeal.divMod_zero_right

added def FractionalIdeal.quotientEquiv

added theorem FractionalIdeal.zero_divMod

added theorem IsDedekindDomain.exists_add_spanSingleton_mul_eq

added theorem IsDedekindDomain.exists_eq_span_pair

added theorem IsDedekindDomain.exists_sup_span_eq

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem FractionalIdeal.sup_mul_inf

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

added theorem FractionalIdeal.coeIdeal_inf