Theorem Set.inv_eq_self_iff_inv_subset

Modification history

2026-03-14 20:09
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
feat(Algebra/Module/Submodule): Add pointwise negation lemma (#36634) …
Added Set.inv_eq_self_iff_inv_subsetView on Github →