Theorems · Theorem · combinatorics

List.destutter.congr_simp

∀ {α : Type u_1} (R R_1 : α → α → Prop),
  R = R_1 →
    ∀ {inst : DecidableRel R} [inst_1 : DecidableRel R_1] (a a_1 : List α),
      a = a_1 → List.destutter R a = List.destutter R_1 a_1

Defined in: Mathlib.Data.List.Destutter
Cited by: 6 results in Mathlib
Foundations: Depth 9 from the axioms · uses Quot.sound
Assumes: DecidableRel

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

List.destutterstatement and proof · cited by 25

Cited by6

Results whose statement or proof uses this declaration.

Polynomial.signVariations_zeroproof · cited by 4
Polynomial.signVariations_negproof · cited by 2
Polynomial.signVariations_eq_eraseLead_add_iteproof · cited by 1
Polynomial.succ_signVariations_le_X_sub_C_mulproof · cited by 1
Polynomial.succ_signVariations_X_sub_C_mul_monomialproof · cited by 0
Polynomial.signVariations_monomialproof · cited by 0