Mathlib Changelog
v4
Changelog
About
Github
Theorem
DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel
Modification history
2026-03-20 16:11
Mathlib/GroupTheory/DoubleCoset.lean
feat(GroupTheory/DoubleCoset): multiple lemmas (#27229) …
Added
DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel
View on Github →