Theorem Finite.exists_type_univ_nonempty_mulEquiv.{u,

Modification history

2025-07-05 07:00
Mathlib/Algebra/Group/TransferInstance.lean
chore(Algebra/Equiv/TransferInstance): split off group results (#26769) …
Added Finite.exists_type_univ_nonempty_mulEquiv.{u,View on Github →