Commit 2026-08-14 20:33 c6d40f21

View on Github →

chore(RingTheory/Ideal/Operations): deprecate duplicate theorem Ideal.span_mul_span' (#39799) Ideal.span_mul_span' is identical to Ideal.span_mul_span.

Estimated changes

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Ideal.span_mul_span'

Modified scripts/nolints_prime_decls.txt