Commit 2026-02-28 14:07 634ad4ee

View on Github →

feat(RingTheory/Ideal/Span): add pair lemmas (#25992) This PR continues the work from #25323. Original PR: https://github.com/leanprover-community/mathlib4/pull/25323

Estimated changes

modified theorem Ideal.map_span
modified theorem Ideal.mem_span_insert'
added theorem Ideal.span_insert_abs
added theorem Ideal.span_insert_neg
added theorem Ideal.span_pair_abs
added theorem Ideal.span_pair_neg
added theorem Ideal.span_pair_zero
modified theorem Ideal.span_singleton_abs
modified theorem Ideal.span_singleton_neg
modified theorem Ideal.span_singleton_zero