Theorems · Definition · group theory

TwoUniqueProds.casesOn

{G : Type u_1} →
  [inst : Mul G] →
    {motive : TwoUniqueProds G → Sort u} →
      (t : TwoUniqueProds G) →
        ((uniqueMul_of_one_lt_card :
              ∀ {A B : Finset G},
                1 < A.card * B.card →
                  ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2) →
            motive ⋯) →
          motive t

Defined in: Mathlib.Algebra.Group.UniqueProds.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Mul

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Finsetstatement and proof · cited by 13,712
Finset.cardstatement and proof · cited by 2,327
SProd.sprodstatement and proof · cited by 1,750
UniqueMulstatement and proof · cited by 28
TwoUniqueProdsstatement and proof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.