Theorems · Inductive type · combinatorics
Multiset.Rel
{α : Type u_1} → {β : Type v} → (α → β → Prop) → Multiset α → Multiset β → PropRel r s t -- lift the relation r between two elements to a relation between s and t,
s.t. there is a one-to-one mapping between elements in s and t following r.
- Defined in
- Mathlib.Data.Multiset.ZeroCons
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
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.
- Multisetstatement · cited by 2,627
Cited by51
Results whose statement or proof uses this declaration.
- UniqueFactorizationMonoid.factors_uniquestatement · cited by 14
- UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvdproof · cited by 8
- Multiset.rel_eqstatement and proof · cited by 6
- Multiset.rel_flipstatement · cited by 6
- Multiset.card_eq_card_of_relstatement and proof · cited by 5
- Multiset.rel_mapstatement · cited by 5
- Multiset.rel_refl_of_refl_onstatement and proof · cited by 5
- Nat.factors_eqproof · cited by 5
- Multiset.rel_map_leftstatement and proof · cited by 4
- Multiset.rel_zero_rightstatement and proof · cited by 4
- UniqueFactorizationMonoid.exists_mem_factors_of_dvdproof · cited by 4
- Multiset.exists_mem_of_rel_of_memstatement and proof · cited by 4