Mathlib Changelog
v4
Changelog
About
Github
Theorem
Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim
Modification history
2022-11-21 03:50
Mathlib/Tactic/Nontriviality/Core.lean
feat: `nontriviality` tactic (#600) …
Added
Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim
View on Github →