Matrix multiplication exponent at most 9/4 over every field

Source: url:https://github.com/jzuiddam/omega-nine-quarters-all-fields/tree/615b591cddd8792173c17b58558ef3b9f11a702c Authors: OpenAI, Jeroen Zuiddam Status: verified Main declarations: MatrixMultiplicationAllFields.omega_le_nine_quarters_all_fields Tags: matrix-multiplication, arithmetic-complexity, tensor-rank, field-extensions MSC: 68Q17, 15A69, 68Q25

theorem MatrixMultiplicationAllFields.omega_le_nine_quarters_all_fields (F : Type u_1) [Field F] : MatrixMultiplication.Arithmetic.omega F ≤ 9 / 4

The matrix multiplication exponent is at most 9/4 over every field.