Commit 2025-10-19 08:57 d95168ed

View on Github →

feat(DedekindDomain/Different): add the transitivity formula (#26155) This PR proves the transitivity formula for the different ideal. The PR also adds one new instance:

FiniteDimensional (FractionRing A) (FractionRing B) deduced from Module.Finite A B.

Estimated changes

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem FractionalIdeal.dual_eq_dual_mul_dual

added theorem FractionalIdeal.smul_mem_dual_one

added theorem FractionalIdeal.trace_mem_dual_one

added theorem differentIdeal_eq_differentIdeal_mul_differentIdeal

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

added theorem FractionalIdeal.extendedHomₐ_coeIdeal_eq_map

added theorem FractionalIdeal.extendedHomₐ_eq_zero_iff

added theorem FractionalIdeal.extended_coeIdeal_eq_map

added theorem FractionalIdeal.extended_eq_zero_iff

added theorem FractionalIdeal.extended_ne_zero

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.map_injective_of_injective'