Theorem star_mem_iff

Modification history

2025-06-21 11:35
Mathlib/Algebra/Star/Basic.lean
feat(Algebra/Star/Basic): star_mem_iff for involutive star (#25863) …
Added star_mem_iffView on Github →