Commit 2026-02-18 23:28 57d8fb21

View on Github →

chore: remove Ideal.span_singleton_le_iff_mem as explicit simp argument (#35498) This PR implements a couple small simp golfs made possible by #35489.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean