instHasAntidiagonal — Mathlib

English

There is a finite antidiagonal structure on Additive PNat, built from divisors of a positive natural number, turning divisors into pairs with positive components and the product relation preserved.

Русский

Существует конечная антидиагональная структура на Additive PNat, построенная через делители положительного натурального числа, переводящая делители в пары с положительными компонентами и сохраняющая равенство произведения.

LaTeX

$$$\text{antidiagonal } n := \text{divisorsAntidiagonal}(n)$ и т.д.$$

Lean4

instance instHasAntidiagonal : Finset.HasAntidiagonal (Additive ℕ+) :=
  /- The set of divisors of a positive natural number.
  This is `Nat.divisorsAntidiagonal` without a special case for `n = 0`. -/

  let divisorsAntidiagonal (n : ℕ+) : Finset (ℕ+ × ℕ+) :=
    (Nat.divisorsAntidiagonal n).attach.map
      ⟨fun x =>
        (⟨x.val.1, Nat.pos_of_mem_divisors <| Nat.fst_mem_divisors_of_mem_antidiagonal x.prop⟩,
          ⟨x.val.2, Nat.pos_of_mem_divisors <| Nat.snd_mem_divisors_of_mem_antidiagonal x.prop⟩),
        fun _ _ h => Subtype.ext <| Prod.ext (congr_arg (·.1.val) h) (congr_arg (·.2.val) h)⟩
  have mem_divisorsAntidiagonal {n : ℕ+} (x : ℕ+ × ℕ+) : x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n :=
    by
    simp_rw [divisorsAntidiagonal, Finset.mem_map, Finset.mem_attach, Function.Embedding.coeFn_mk, Prod.ext_iff,
      true_and, ← coe_inj, Subtype.exists]
    simp
  { antidiagonal := fun n ↦
      divisorsAntidiagonal (Additive.toMul n) |>.map
        (.prodMap (Additive.ofMul.toEmbedding) (Additive.ofMul.toEmbedding))
    mem_antidiagonal := by simp [← ofMul_mul, mem_divisorsAntidiagonal] }

Похожие утверждения