English
For a semiring α, given n and y, CPRankMax n y is preserved under left multiplication by x in Holor α [d] when ds is a singleton: CPRankMax n y → CPRankMax n (x ⊗ y).
Русский
При умножении слева на x при Holor α [d] с единичным списком ds сохраняется CPRankMax n y → CPRankMax n (x ⊗ y).
LaTeX
$$$$ CPRankMax n y \\rightarrow CPRankMax n (x \\otimes y) $$$$
Lean4
theorem cprankMax_mul [NonUnitalNonAssocSemiring α] :
∀ (n : ℕ) (x : Holor α [d]) (y : Holor α ds), CPRankMax n y → CPRankMax n (x ⊗ y)
| 0, x, _, CPRankMax.zero => by simp [mul_zero x, CPRankMax.zero]
| n + 1, x, _, CPRankMax.succ _ y₁ y₂ hy₁ hy₂ =>
by
rw [mul_left_distrib]
rw [Nat.add_comm]
apply cprankMax_add
· exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)
· exact cprankMax_mul _ x y₂ hy₂
