circulantGraph_eq_erase_zero — Mathlib

English

Removing 0 from the jump set s does not change the circulant graph.

Русский

Удаление нуля из множества прыжков s не изменяет циркулярный граф.

LaTeX

$$circulantGraph(s) = circulantGraph(s \ {0})$$

Lean4

theorem circulantGraph_eq_erase_zero : circulantGraph s = circulantGraph (s \ {0}) :=
  by
  ext (u v : G)
  simp only [circulantGraph, fromRel_adj, and_congr_right_iff]
  intro (h : u ≠ v)
  apply Iff.intro
  · intro h1
    cases h1 with
    | inl h1 => exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩
    | inr h1 => exact Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩
  · intro h1
    cases h1 with
    | inl h1 => exact Or.inl h1.left
    | inr h1 => exact Or.inr h1.left

Похожие утверждения