Theorem MulAction.pretransitive_iff_unique_quotient_of_nonempty

Modification history

2024-02-08 17:51
Mathlib/GroupTheory/GroupAction/Basic.lean
feat(CategoryTheory/Galois): definition and characterisation of Galois objects (#10215) …
Added MulAction.pretransitive_iff_unique_quotient_of_nonemptyView on Github →