:: deftheorem Def12 defines ACirc MATRIX16:def 12 :
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
for b₃ being Matrix of len p,K holds
( b₃ = ACirc p iff b₃ is_anti-circular_about p );