Mathlib don't have the tactic like "rank_smul"?

Stream: new members

[Hbz]

import Mathlib

open Matrix

variable {n : Type} [Fintype n] [DecidableEq n] {R : Type} [Field R]

lemma A_k_eq_A (A : Matrix n n R) (hA : A * A = A) (k : ℕ) (hk : k ≥ 1):
  A ^ k = A := by
  induction' k with k ih
  ·
    exfalso
    exact Nat.not_succ_le_zero 0 hk
  ·
    by_cases hk0 : k = 0
    ·
      rw[hk0]
      simp
    ·
      have hk_d1 : k ≥ 1 := by exact Nat.one_le_iff_ne_zero.mpr hk0
      exact IsIdempotentElem.pow_succ_eq k hA

#leansearch "A.rank = (-A).rank?"
variable (B:Matrix n n R)
#check B.transpose
lemma subI_pow_rank_eq (A : Matrix n n R) (hA : A * A = A) (m : ℕ) (m_pos : m ≥ 1) :
   ((A - 1)^m).rank = (A - 1).rank := by
  have h : (A - 1) * (A - 1) = -(A - 1) := by
    simp[mul_sub,sub_mul,hA]
  induction' m with m ih
  ·
    exfalso
    exact Nat.not_succ_le_zero 0 m_pos
  ·
    rcases Nat.even_or_odd m with ⟨m, rfl⟩ | ⟨m, rfl⟩
    ·

      sorry
    ·
      have h1 : (A - 1) ^ (2 * m + 1 + 1) = 1 - A := by

        sorry
      sorry

-- 辅助引理3：幂等矩阵A与(A-I)的秩之和等于n
lemma idempotent_rank_sum (A : Matrix n n R)
  (hA : A * A = A) :
  A.rank + (A - 1).rank = Fintype.card n := by
  have h_le : A.rank + (A - 1).rank ≤ Fintype.card n := by
    sorry
  have h_ge : A.rank + (A - 1).rank ≥ Fintype.card n := by
    sorry
  sorry  -- 利用秩的基本性质证明


theorem rank_sum_of_idempotent (A : Matrix n n R) (hA : A * A = A)
    (k l : ℕ) (hk : k ≥ 1) (hl : l ≥ 1) :
    (A ^ k).rank + ((A - 1) ^ l).rank = Fintype.card n := by
  have h1 : A ^ k = A := by
    exact A_k_eq_A A hA k hk
  rw[h1]
  have h2 : ((A - 1) ^ l).rank = (A - 1).rank := by
    exact subI_pow_rank_eq A hA l hl
  rw[h2]
  exact idempotent_rank_sum A hA

I want to show that (A - 1).rank=(1 - A).rank or (A - 1).rank = (c * (A - 1)).rank,but i didn't find the right tactic.
So, enn, does it exist? :slight_smile:

[Niels Voss]

Yeah, I wasn't able to find anything that's in the form you want. The closest thing seems to be docs#LinearMap.range_smul. If you unfold the definition of LinearMap.rank, then you should be able to use the fact that the ranges are equal to conclude that the ranks are equal

[Niels Voss]

Or in this case, you can use docs#LinearMap.range_neg

[Hbz]

Thank you!