Mathlib Changelog
v4
Changelog
About
Github
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 →