cprankMax_1

Mathlib.Data.Holor

URI: https://scilib.ai/kg/mathlib#Holor.cprankMax_1

← MathLib Explorer

English

If x has CPRankMax1, then its CP-rank is 1: CPRankMax 1 x.

Русский

Если у x CPRankMax1, то его CP-ранг равен 1: CPRankMax 1 x.

LaTeX

$$$$ CPRankMax 1 x $$$$

Lean4

theorem cprankMax_1 [Mul α] [AddMonoid α] {x : Holor α ds} (h : CPRankMax1 x) : CPRankMax 1 x :=
  by
  have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
  rwa [zero_add, add_zero] at h'

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru