Mixed Signed Entry Good swap

Proved

D1Bound5.mixedSignedEntryGood_swap

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

diophantine-tuplesnumber-theory

Auxiliary result mixedSignedEntryGood_swap in the proof of the bound five for Diophantine D(1) sets in imaginary quadratic integer rings. The formal statement specifies its hypotheses and conclusion; a mathematical prose description remains to be supplied.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_MixedRootMatrixSigns_Definitions

Formal statement

section
namespace D1Bound5













theorem _root_.D1Bound5.mixedSignedEntryGood_swap {R : Type*} [CommRing R]
    (f : R →+* ℂ) (a : Fin 4 → R) (u : Fin 4 → ℂ)
    (i j : Fin 4) (r : R)
    (h : MixedSignedEntryGood f a u i j r) :
    MixedSignedEntryGood f a u j i r := by sorry



end D1Bound5
namespace D1Bound5





end D1Bound5
end

Source

D1Bound5/MixedRootMatrixSigns.lean, lines 92-107, SHA-256 2e004ca5529f8e5abf67259e26a8270075f09b04d9c8093e81458a83e3680457. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph