Commit 2025-08-19 22:25 5235abbc

feat(RingTheory/Ideal/Span): some lemmas about zero and span (#26148) simp would be able to solve them. Notice that span_singleton_zero : span {(0 : R)} = ⊥ itself can be solved by simp without this commit, which uses span_singleton_eq_bot : span ({x} : Set α) = ⊥ ↔ x = 0, while simp cannot solve goals like f (Ideal.span {(0 : R)}) = f ⊥, which would be solvable by simp with span_singleton_zero marked with @[simp]. Without adding also Ideal.dvd_bot, these lemmas on Span.lean would make the following failed, since simp would rewrite {0} with ⊥ and result in a goal v.asIdeal ∣ ⊥ that it can't solve. https://github.com/leanprover-community/mathlib4/blob/3f2556372f27171259a381d4d57db71440700cd8/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean#L123