Commit 2025-06-21 11:35 8f5e35a6

feat(Algebra/Star/Basic): star_mem_iff for involutive star (#25863) added lemma: star x ∈ s iff x ∈ s