Theorem Finite.exists_type_zero_nonempty_mulEquiv

Modification history

2024-09-12 17:39

Mathlib/Logic/Equiv/TransferInstance.lean

feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) …

Deleted Finite.exists_type_zero_nonempty_mulEquiv View on Github →

2024-01-24 14:31

Mathlib/Logic/Equiv/TransferInstance.lean

feat(CategoryTheory/Galois): finite `G`-sets are a `PreGaloisCategory` (#9879) …

Added Finite.exists_type_zero_nonempty_mulEquiv View on Github →