The full theorem in the independent Mathlib vocabulary #
Both directions of special biseriality preserve the displayed quiver and Morita equivalence. Together with the numerical connections, this derives the independent statement from the production theorem.
theorem
MagnitudeConjecture.Statement.isSpecialBiserial_iff
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
:
The independent special-biserial predicate has exactly the production meaning, including the Morita-class convention for nonbasic algebras.
theorem
MagnitudeConjecture.Statement.mainClaim
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsAlgClosed k]
:
MainClaim k A
The magnitude theorem with independent definitions: nonsingularity of the Hom matrix, the lower bound by simple classes, and the full equality case.