This file is generated from the following operator table: [[3,4,1,2,0], [2,0,4,1,3], [0,1,2,3,4], [1,3,0,4,2], [4,2,3,0,1]]

The magma definition

def «FinSearch [[3,4,1,2,0], [2,0,4,1,3], [0,1,2,3,4], [1,3,0,4,2], [4,2,3,0,1]]» : Magma (Fin 5)

Equations

• One or more equations did not get rendered due to their size.

The facts

theorem «Facts from FinSearch [[3,4,1,2,0], [2,0,4,1,3], [0,1,2,3,4], [1,3,0,4,2], [4,2,3,0,1]]» : ∃ (G : Type) (x : Magma G) (_ : Finite G), Equation231 G ∧ Equation620 G ∧ Equation633 G ∧ Equation670 G ∧ Equation704 G ∧ Equation826 G ∧ Equation833 G ∧ Equation880 G ∧ Equation919 G ∧ Equation1435 G ∧ Equation1445 G ∧ Equation1452 G ∧ Equation1479 G ∧ Equation3091 G ∧ Equation3140 G ∧ Equation3201 G ∧ Equation4276 G ∧ Equation4362 G ∧ Equation4608 G ∧ ¬Equation47 G ∧ ¬Equation99 G ∧ ¬Equation151 G ∧ ¬Equation211 G ∧ ¬Equation221 G ∧ ¬Equation255 G ∧ ¬Equation411 G ∧ ¬Equation619 G ∧ ¬Equation622 G ∧ ¬Equation623 G ∧ ¬Equation629 G ∧ ¬Equation630 G ∧ ¬Equation632 G ∧ ¬Equation639 G ∧ ¬Equation640 G ∧ ¬Equation642 G ∧ ¬Equation643 G ∧ ¬Equation667 G ∧ ¬Equation669 G ∧ ¬Equation676 G ∧ ¬Equation677 G ∧ ¬Equation679 G ∧ ¬Equation680 G ∧ ¬Equation706 G ∧ ¬Equation707 G ∧ ¬Equation819 G ∧ ¬Equation825 G ∧ ¬Equation832 G ∧ ¬Equation835 G ∧ ⋯