Theorem Finite.exists_type_univ_nonempty_mulEquiv

Modification history

2024-09-12 17:39
Mathlib/Logic/Equiv/TransferInstance.lean
feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) …
Added Finite.exists_type_univ_nonempty_mulEquivView on Github →