Theorem Subsingleton.eq_one

Modification history

2023-09-05 09:13
Mathlib/Logic/Nontrivial/Basic.lean
feat: split Logic.Nontrivial (#6959) …
Modified Subsingleton.eq_oneView on Github →
2023-07-28 16:09
Mathlib/Logic/Nontrivial.lean
feat(RingTheory/Polynomial/ScaleRoots): reduce typeclass assumptions (#6213)
Added Subsingleton.eq_oneView on Github →