no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α [d]
⊢ CPRankMax 0 (x ⊗ 0)
simp [mul_zero x, CPRankMax.zero]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ (y₁ + y₂))
rw [mul_left_distrib]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
rw [Nat.add_comm]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)

case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
apply cprankMax_add
no goals
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)
exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)
no goals
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)
exact cprankMax_mul _ x y₂ hy₂