cprank_upper_bound — Mathlib

English

For rings, cprank x ≤ ds.prod, i.e., the CP-rank does not exceed the product of the dimension list.

Русский

Для колец cprank x ≤ ds.prod, то есть CP-ранг не превышает произведение элементов ds.

LaTeX

$$$$ \\text{cprank}(x) \\le ds.prod $$$$

Lean4

theorem cprank_upper_bound [Ring α] : ∀ {ds}, ∀ x : Holor α ds, cprank x ≤ ds.prod := fun {ds} x =>
  letI := Classical.decPred fun n : ℕ => CPRankMax n x
  Nat.find_min' ⟨ds.prod, show (fun n => CPRankMax n x) ds.prod from cprankMax_upper_bound x⟩ (cprankMax_upper_bound x)

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