Commit 2025-06-16 08:23 cdcb17b4

View on Github →

feat(RingTheory): Order of vanishing in a ring (#25255) In this PR we define the order of vanishing of a ring and its extension to elements of the function field (as in stacks project 02MD) as well as some basic API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithBot.add_le_add_iff_right'

Modified Mathlib/RingTheory/Artinian/Module.lean

added theorem isArtinian_of_surjective_algebraMap

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.range_mul'

added theorem Ideal.range_mul

added theorem Submodule.smul_le_span

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

added theorem Ideal.Quotient.smul_top

Created Mathlib/RingTheory/OrderOfVanishing.lean

added theorem Ideal.exact_mulQuot_quotOfMul

added def Ideal.mulQuot

added theorem Ideal.mulQuot_injective

added def Ideal.quotOfMul

added theorem Ideal.quotOfMul_surjective

added def Ring.ord

added def Ring.ordFrac

added theorem Ring.ordFrac_eq_div

added theorem Ring.ordFrac_eq_ord

added def Ring.ordMonoidWithZeroHom

added theorem Ring.ord_mul

added theorem Ring.ord_one

added theorem isFiniteLength_quotient_span_singleton