Source labels openOther · Mathematics
Equational Theories: Equation677 Not Implies Equation255
The negation of Finite.Equation677_implies_Equation255.
Probably this is true. It would be a stronger form of
Equation677_not_implies_Equation255.
Discussion thread here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255
Source checked Jul 26, 20261 pinned Lean statementInspect problem