Complex arithmetic interfaces specialized from the shared field-generic implementation.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.AdmissibleExponent.mono {τ σ : ℝ} (hτ : AdmissibleExponent τ) (hτσ : τ ≤ σ) : AdmissibleExponent σ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_le_of_admissibleExponent {τ : ℝ} (hτ : AdmissibleExponent τ) : omega ≤ τ

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_nonneg : 0 ≤ omega

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_le_three : omega ≤ 3

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.omega_admissibleExponent : AdmissibleExponent omega

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Arithmetic.admissibleExponent_iff_omega_le {τ : ℝ} : AdmissibleExponent τ ↔ omega ≤ τ