mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PD l R)ᵀ * JD l R * PD l R = 2 • S l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ IsUnit A.det

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝⁵ : DecidableEq l
inst✝⁴ : Fintype l
inst✝³ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
F : Type u_3
S : Type u_4
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
hA : A ∈ symplecticGroup l R
f : F
⊢ A.map ⇑f ∈ symplecticGroup l S

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
⊢ IsUnit Aᵀ.det

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PD l R * ⅟2 • (PD l R)ᵀ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PD l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A = -(J l R)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit A.det
huAT : IsUnit Aᵀ.det
⊢ -(J l R)⁻¹ = J l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ Aᵀ ∈ symplecticGroup l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
rw [mem_iff'] at hA
      rw [hA]

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * J l R = -1 • (J l R * J l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • (J l R * J l R) = -1 • -1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • -1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↥(typeD l R) ≃ₗ⁅R⁆ ↥(so' l l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : ↥(symplecticGroup l R)
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * Aᵀ * J l R * A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : ↥(symplecticGroup l R)
⊢ A⁻¹ * A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ range ((A.submatrix r id).submatrix id c).col ⊆ range (A.submatrix r id).col

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : fromBlocks A B C D ∈ symplecticGroup l R
⊢ fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D) (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : fromBlocks A B C D ∈ symplecticGroup l R
h_final : fromBlocks (Cᵀ * A - Aᵀ * C) (Cᵀ * B - Aᵀ * D) (Dᵀ * A - Bᵀ * C) (Dᵀ * B - Bᵀ * D) = J l R
h_eq1 : Cᵀ * A - Aᵀ * C = 0
h_eq2 : Cᵀ * B - Aᵀ * D = -1
left✝ : Dᵀ * A - Bᵀ * C = 1
h_eq3 : Dᵀ * B - Bᵀ * D = 0
⊢ Aᵀ * D - Cᵀ * B = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
h : ((A.submatrix r id).submatrix id c).cRank ≤ (A.submatrix r id).cRank
f : (m → R) →ₗ[R] m₀ → R := LinearMap.funLeft R R r
⊢ Submodule.map f (span R (range A.col)) = span R (range (A.submatrix r id).col)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (PB l R)ᵀ * JB l R * PB l R = 2 • fromBlocks 1 0 0 (S l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ Cᵀ * B - Aᵀ * D = -1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
h : Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1
⊢ Dᵀ * A - Bᵀ * C = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A B C D : Matrix l l R
⊢ fromBlocks A B C D ∈ symplecticGroup l R ↔ Aᵀ * C = Cᵀ * A ∧ Bᵀ * D = Dᵀ * B ∧ Aᵀ * D - Cᵀ * B = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ lift.{um₀, max uR um} A.cRank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
m m₀ : Type um
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).cRank ≤ A.cRank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype m
A : Matrix m n R
⊢ Module.rank R (m → R) ≤ ↑(Fintype.card m)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n
A : Matrix m n R
⊢ #↑(range A.col) ≤ ↑(Fintype.card n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : Subsingleton R
A : Matrix m n R
⊢ A.eRank = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).eRank ≤ A.eRank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite n → A.eRank ≤ ENat.card n
hfin : ¬Finite n
⊢ Infinite ?m.33

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝³ : DecidableEq l
inst✝² : Fintype l
inst✝¹ : CommRing R
A B C D : Matrix l l R
inst✝ : Invertible A
hA : fromBlocks A B C D ∈ symplecticGroup l R
⊢ (fromBlocks A B C D).det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
this :
  ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] [StrongRankCondition R] (A : Matrix m n R),
    Finite m → A.eRank ≤ ENat.card m
hfin : ¬Finite m
⊢ Infinite ?m.33

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
⊢ A.eRank ≤ ENat.card m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ LinearIndependent R (col 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ cRank 1 = lift.{uR, um} #m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
⊢ eRank 1 = ENat.card m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : DecidableEq n
inst✝ : StrongRankCondition R
⊢ rank 1 = Fintype.card n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ rank 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ cRank 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: R : Type uR
m : Type u_1
n : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ eRank 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ A.rank

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: l : Type u_4
R : Type u₂
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ indefiniteDiagonal (Unit ⊕ l) l R =
    (reindexLieEquiv (Equiv.sumAssoc Unit l l).symm) (fromBlocks 1 0 0 (indefiniteDiagonal l l R))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ Invertible (PB l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
a✝ : Nontrivial R
⊢ finrank R ↥(A.mulVecLin ∘ₗ B.mulVecLin).range ≤ finrank R ↥B.mulVecLin.range

Tactic:
exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
    (rank_lt_aleph0 _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
o : Type uo
R : Type uR
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
R : Type uR
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
w : m → R
v : n → R
⊢ (vecMulVec w v).rank ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : (Matrix n n R)ˣ
⊢ (↑A).rank = Fintype.card n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: n : Type un
R : Type uR
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StrongRankCondition R
A : Matrix n n R
h : IsUnit A
⊢ A.rank = Fintype.card n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
R : Type u_1
inst✝³ : CommRing R
inst✝² : Nontrivial R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
hA : A.det ∈ nonZeroDivisors R
⊢ A.rank = Fintype.card m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
hc' : IsSMulRegular R c
hreg : IsSMulRegular (m → R) c
f : (m → R) →ₗ[R] m → R := (LinearMap.lsmul R (m → R)) c
⊢ (c • B).mulVecLin = f ∘ₗ B.mulVecLin

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: n : Type u_1
p : Type u_2
q : Type u_3
l : Type u_4
R : Type u₂
inst✝⁸ : DecidableEq p
inst✝⁷ : DecidableEq q
inst✝⁶ : DecidableEq l
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq n
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ ↥(typeB l R) ≃ₗ⁅R⁆ ↥(so' (Unit ⊕ l) l R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝¹ : Fintype n
R : Type u_1
inst✝ : CommRing R
c : R
B : Matrix m n R
hc : c ∈ nonZeroDivisors R
⊢ (c • B).rank = B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
⊢ B * A * A.adjugate = A.det • B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
a✝ : Nontrivial R
key : B * A * A.adjugate = A.det • B
⊢ (A.det • B).rank = (B * A * A.adjugate).rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝² : Fintype n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ (B * A).rank = B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝³ : Fintype n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
B : Matrix m n R
hA : A.det ∈ nonZeroDivisors R
⊢ (A * B).rank = B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝⁴ : Fintype n
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Fintype m
inst✝ : LinearOrder m
A : Matrix m m R
B : Matrix m n R
hA : A.IsLowerTriangular
hd : ∀ (i : m), A.diag i ≠ 0
⊢ A.det ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝⁴ : Fintype n
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Fintype m
inst✝ : LinearOrder m
A : Matrix m m R
B : Matrix m n R
hA : A.IsLowerTriangular
hd : ∀ (i : m), A.diag i ≠ 0
⊢ (A * B).rank = B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝⁴ : Fintype n
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Fintype m
inst✝ : LinearOrder m
A : Matrix m m R
B : Matrix m n R
hA : A.IsUpperTriangular
hd : ∀ (i : m), A.diag i ≠ 0
⊢ A.det ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
n : Type un
inst✝⁴ : Fintype n
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Fintype m
inst✝ : LinearOrder m
A : Matrix m m R
B : Matrix m n R
hA : A.IsUpperTriangular
hd : ∀ (i : m), A.diag i ≠ 0
⊢ (A * B).rank = B.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r c).rank = ((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ ((A.submatrix r id)ᵀᵀ.submatrix id c)ᵀᵀ.rank ≤ finrank R ↥(span R (range (A.submatrix r id).col))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ finrank R ↥(span R (range (A.submatrix r id).col)) = (A.submatrix r id)ᵀᵀ.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
a✝ : Nontrivial R
this : Module.Finite R ↥(span R (range (A.submatrix r id).col))
⊢ (A.submatrix r id)ᵀᵀ.rank = (A.submatrix r ⇑(Equiv.refl n)).rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝³ : Fintype n
inst✝² : CommSemiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype n₀
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).rank ≤ A.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
em : m ≃ m₀
en : n ≃ n₀
A : Matrix m n R
⊢ ((reindex em en) A).rank = A.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n : Type un
n₀ : Type un₀
R : Type uR
inst✝² : Fintype n
inst✝¹ : Fintype n₀
inst✝ : CommSemiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ (A.submatrix ⇑em ⇑en).rank = A.rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Rank

Goal state before:
pp: m : Type um
m₀ : Type um₀
n₀ : Type un₀
R : Type uR
n : Type un
inst✝ : Semiring R
A : Matrix m n R
em : m₀ ≃ m
en : n₀ ≃ n
⊢ lift.{um₀, max uR um} A.cRank ≤ lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank

Tactic:
by

Goal state after: