Theorems · Theorem · combinatorics

Multiset.sort.congr_simp

∀ {α : Type u_1} (s s_1 : Multiset α),
  s = s_1 →
    ∀ (r r_1 : α → α → Prop) (e_r : r = r_1) {inst : DecidableRel r} [inst_1 : DecidableRel r_1] [inst_2 : IsTrans α r]
      [inst_3 : Std.Antisymm r] [inst_4 : Std.Total r], s.sort r = s_1.sort r_1

Defined in: Mathlib.Data.Multiset.Sort
Cited by: 3 results in Mathlib
Foundations: Depth 60 from the axioms · uses propext, Quot.sound
Assumes: DecidableRel IsTrans Std.Antisymm Std.Total

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

Multisetstatement and proof · cited by 2,627
IsTransstatement and proof · cited by 157
Multiset.sortstatement and proof · cited by 19

Cited by3

Results whose statement or proof uses this declaration.

LinearMap.IsSymmetric.sort_roots_charpoly_eq_eigenvaluesproof · cited by 1
Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀proof · cited by 0
Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iffproof · cited by 0