Def DoubleCoset.quotToDoubleCoset

Modification history

2026-07-24 07:15
Mathlib/GroupTheory/DoubleCoset.lean
chore: add missing `noncomputable` (#41446) …
Deleted DoubleCoset.quotToDoubleCosetView on Github →
2025-08-03 03:08
Mathlib/GroupTheory/DoubleCoset.lean
chore: rename doset to doubleCoset (#27004)
Added DoubleCoset.quotToDoubleCosetView on Github →