Formal target: Corpus.Arxiv160103081UniqueCrystalComponents.crystals_components_unique

If $n = ab$ is a crystal, then there are no other pairs of positive integers $c, d > 1$, different from the couple $a, b$, such that $n = cd$ and $B(c, d) ∈ ℕ$, i.e., the components of the crystals are unique.

Exact formal statement

∀ (n a b c d : Nat),
  Corpus.Arxiv160103081UniqueCrystalComponents.IsCrystalWithComponents n a b →
    Corpus.Arxiv160103081UniqueCrystalComponents.IsCrystalWithComponents n c d →
      Eq.{1} (Insert.insert.{0, 0} a (Singleton.singleton.{0, 0} b))
        (Insert.insert.{0, 0} c (Singleton.singleton.{0, 0} d))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record