Theorem Subsingleton.eq_one

Modification history

2025-03-08 08:24
Mathlib/Algebra/Notation/Defs.lean
chore: create the `Algebra.Notation` folder (#22640) …
Modified Subsingleton.eq_oneView on Github →
2024-12-20 12:30
Mathlib/Algebra/Group/ZeroOne.lean
chore: revert import order between Algebra.Group.ZeroOne and Logic.Nonempty (#19994)
Modified Subsingleton.eq_oneView on Github →
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 →