Theorem Equiv.nontrivial_congr

Modification history

2025-05-01 06:42
Mathlib/Logic/Equiv/Defs.lean
feat: preliminaries for Wedderburn–Artin (#24119)
Added Equiv.nontrivial_congrView on Github →