Theorem DoubleCoset.out_eq'

Modification history

2026-09-03 10:12
Mathlib/GroupTheory/DoubleCoset.lean
chore(GroupTheory): make arguments implicit in two iff lemmas (#43382) …
Modified DoubleCoset.out_eq'View on Github →
2026-03-20 16:11
Mathlib/GroupTheory/DoubleCoset.lean
feat(GroupTheory/DoubleCoset): multiple lemmas (#27229) …
Modified DoubleCoset.out_eq'View on Github →
2025-08-03 03:08
Mathlib/GroupTheory/DoubleCoset.lean
chore: rename doset to doubleCoset (#27004)
Added DoubleCoset.out_eq'View on Github →