Theorems · Theorem · number theory

Behrend.map_eq_iff

∀ {n d : ℕ} {x₁ x₂ : Fin n.succ → ℕ},
  (∀ (i : Fin n.succ), x₁ i < d) →
    (∀ (i : Fin n.succ), x₂ i < d) →
      ((Behrend.map d) x₁ = (Behrend.map d) x₂ ↔
        x₁ 0 = x₂ 0 ∧ (Behrend.map d) (x₁ ∘ Fin.succ) = (Behrend.map d) (x₂ ∘ Fin.succ))

Defined in

Mathlib.Combinatorics.Additive.AP.Three.Behrend

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound