Finite MTerms admissible

Proved

D1Bound5.finiteMTerms_admissible

by tp · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

Every root-column monomial has the required anchor and terminal weights.

Preamble

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FiniteMMatrix_Definitions

Formal statement

section
namespace D1Bound5




















theorem _root_.D1Bound5.finiteMTerms_admissible (i : Fin 4) (j : Fin 3) :
    ∀ t ∈ finiteMTerms i j.succ, finiteMTermAdmissible t := by sorry








end D1Bound5
end

Source

D1Bound5/FiniteMMatrix.lean, lines 145-148, SHA-256 8af7f9699b9fc84a48e57a25795d84c9aefe6f4ade8e20a65b9b82216db511c9. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph