cprankMax_nil — Mathlib

English

For any semiring structure, if the shape is nil (empty index list), then CPRankMax 1 x holds for any x.

Русский

Для любой полугруппы с умножением: если форма пустая (nil), то CPRankMax 1 x выполняется для любого x.

LaTeX

$$$$ CPRankMax 1 x $$$$

Lean4

theorem cprankMax_nil [Mul α] [AddMonoid α] (x : Holor α nil) : CPRankMax 1 x :=
  by
  have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero
  rwa [add_zero x, zero_add] at h

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