Commit 2026-04-17 19:17 c4037aa6

View on Github →

chore: make Ideal.span an abbrev (#38145)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Modified Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Bezout.lean

Modified Mathlib/RingTheory/Ideal/Colon.lean

modified theorem Ideal.colon_span

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

Modified Mathlib/RingTheory/Ideal/NatInt.lean

Modified Mathlib/RingTheory/Ideal/Span.lean

modified theorem Ideal.mem_span_singleton_self

deleted def Ideal.span

modified theorem Ideal.span_empty

modified theorem Ideal.span_eq

modified theorem Ideal.span_eq_bot

modified theorem Ideal.span_insert_zero

modified theorem Ideal.span_sdiff_singleton_zero

modified theorem Ideal.span_singleton_eq_bot

modified theorem Ideal.span_singleton_le_iff_mem

modified theorem Ideal.span_singleton_zero

modified theorem Ideal.span_univ

modified theorem Ideal.span_zero

modified theorem Ideal.submodule_span_eq

Modified Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/RingTheory/Valuation/Discrete/Basic.lean

Modified Mathlib/RingTheory/Valuation/Integers.lean