Theorem DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ

Modification history

2026-03-20 16:11
Mathlib/GroupTheory/DoubleCoset.lean
feat(GroupTheory/DoubleCoset): multiple lemmas (#27229) …
Added DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univView on Github →