mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Goal state before:
pp: m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = #{i | cert.pivot i ≠ ⊤}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
htri : (A.submatrix Subtype.val g).IsUpperTriangular
⊢ (A.submatrix Subtype.val g).det ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
htri : (A.submatrix Subtype.val g).IsUpperTriangular
hdet : (A.submatrix Subtype.val g).det ≠ 0
⊢ #{i | l i ≠ ⊤} = (A.submatrix Subtype.val g).rank

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
⊢ A.rank = #{i | l i ≠ ⊤}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
⊢ (A.fromRows B).IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
h : Nonempty n
i j : n
⊢ 1 i j = Pi.single i (↑1) j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
⊢ fromRows 1 A = (reindex (Equiv.sumComm m n) (Equiv.refl n)) (A.fromRows 1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
⊢ (fromRows 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (A.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (fromCols 1 A).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
⊢ (p - q) * (Matrix.mvPolynomialX m m k).det = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
⊢ p = q

Tactic:
by
  have hprod : (p - q) * Matrix.det (Matrix.mvPolynomialX m m k) = 0 := by
    apply MvPolynomial.funext
    intro s
    rw [map_mul, map_sub, map_zero, Matrix.eval_det_mvPolynomialX]
    by_cases hs_det : Matrix.det (Matrix.of fun i j : m => s (i, j)) = 0
    · rw [hs_det, mul_zero]
    · have hh : (eval s) p = (eval s) q :=
        h (Matrix.GeneralLinearGroup.mkOfDetNeZero
          (Matrix.of fun i j : m => s (i, j)) hs_det)
      rw [hh, sub_self, zero_mul]
  exact sub_eq_zero.mp
    ((mul_eq_zero.mp hprod).resolve_right (Matrix.det_mvPolynomialX_ne_zero m k))

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ↑A = ↑B
⊢ A = B

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
A B : FixedDetMatrix n R m
h : ∀ (i j : n), ↑A i j = ↑B i j
⊢ A = B

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ (↑g * ↑A).det = m

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
x y : SpecialLinearGroup n R
b : FixedDetMatrix n R m
⊢ (x * y) • b = x • y • b

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
b : FixedDetMatrix n R m
⊢ 1 • b = b

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ ↑(g • A) = ↑g * ↑A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ = q ^ n - q ^ k

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
this : ↑(reduceStep A) 1 0 = ↑A 0 0 % ↑A 1 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ Nat.card { s // LinearIndependent K s } = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ LinearIndependent 𝔽 (↑M).col

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 ≠ 0
⊢ |↑(reduceStep A) 1 0| < |↑A 1 0|

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
⊢ IsUnit (↑M)ᵀ.det

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
⊢ Function.RightInverse (fun M ↦ GeneralLinearGroup.mk'' (↑M)ᵀ ⋯) fun M ↦ ⟨(↑M).col, ⋯⟩

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
⊢ C A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
⊢ Nat.card (GL (Fin n) 𝔽) = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ reduce A = T ^ (-(↑A 0 1 / ↑A 1 1)) • A

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : ¬0 < ↑A 0 0
⊢ reduce A = T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ reduce (reduceStep A) = reduce A

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
ha : ↑A 1 0 = 0
⊢ ↑A 0 0 * ↑A 1 1 = m

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ A.den ≠ 0

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ A.num = 0 ↔ A = 0

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
r : ℕ
⊢ A.den ∣ r ↔ ∀ (i : m) (j : n), (A i j).den ∣ r

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ ↑A i j ∈ Finset.Icc (-|m|) |m|

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i : m
j : n
⊢ ↑(A.num i j) / ↑A.den = A i j

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (↑A.den)⁻¹ • A.num.map Int.cast = A

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ ∀ (c : ℕ), (-A).den ∣ c ↔ A.den ∣ c

Tactic:
by

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

Goal state before:
pp: A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : |↑A 0 1| < 0
⊢ False

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (-A).num = -A.num

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
x✝ : ℕ
⊢ Aᵀ.den ∣ x✝ ↔ A.den ∣ x✝

Tactic:
by

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

Goal state before:
pp: ⊢ reps 0 = ∅

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ Aᵀ.num = A.numᵀ

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℤ
⊢ (A.map Int.cast).den = 1

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℤ
⊢ (A.map Int.cast).num = A

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℕ
⊢ (A.map Nat.cast).den = 1

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℕ
⊢ (A.map Nat.cast).num = A.map Nat.cast

Tactic:
by

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

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (↑a).den = 1

Tactic:
by

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

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (↑a).num = ↑a

Tactic:
by

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

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (↑a).den = 1

Tactic:
by

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

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℤ
⊢ (↑a).num = ↑a

Tactic:
by

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m k : ℤ
⊢ Fintype ↑(reps k)

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • S • A = A

Tactic:
by

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

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
⊢ S • S • S • T • S • T • S • A = T⁻¹ • A

Tactic:
by

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

Goal state before:
pp: m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : 0 < ↑A 0 0
n : ℤ := ↑A 0 1 / ↑A 1 1
h2 : ↑A 0 1 % ↑A 1 1 = ↑A 0 1 - ↑A 1 1 * n
h4 : n * ↑A 1 1 ≤ ↑A 0 1
h3 : |↑A 0 1 % ↑A 1 1| < |↑A 1 1|
this : ↑A 1 0 = 0 ∧ n * ↑A 1 0 < ↑A 0 0 ∧ n * ↑A 1 1 ≤ ↑A 0 1 ∧ |↑A 0 1 + -(n * ↑A 1 1)| < |↑A 1 1|
⊢ ⟨!![1, -n; 0, 1] * ↑A, ⋯⟩ ∈ reps m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
⊢ p₁.length ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₁ : Path i v
p₂ : Path v j
_hp_eq : p = p₁.comp p₂
hp₁_len : p₁.length = 1
hlen_ne : p₁.length ≠ 0
⊢ p₁.length ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ p'.length = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
⊢ v i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
⊢ ∃ j, 0 < A i j

Tactic:
by

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

Goal state before:
pp: m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
⊢ reduce A ∈ reps m

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
j : n
⊢ ‖v j * (v i)⁻¹‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) ↔ C B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
⊢ ∃ l ∈ Finset.univ, 0 < (A ^ m) i l * A l j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
⊢ 0 < (A ^ m) i l

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
⊢ 0 < A l j

Tactic:
by

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) ↔ C B

Tactic:
by

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ ‖A i i - μ‖ = ‖(A i i * v i - μ * v i) * (v i)⁻¹‖

Tactic:
by

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Commute (star A) A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j l : n
hl_mem : l ∈ Finset.univ
hA_nonneg' : 0 ≤ A l j
h_A : 0 < A l j
p : Path i l
ih : ∀ (i_1 j : n), 0 < (A ^ p.length) i_1 j ↔ Nonempty { p_1 // p_1.length = p.length }
h_pos : 0 < ∑ j_1, (A ^ p.length) i j_1 * A j_1 j
hl_pos : 0 < (A ^ p.length) i l * A l j
hAm_nonneg : 0 ≤ (A ^ p.length) i l
h_Am : 0 < (A ^ p.length) i l
⊢ (p.cons { down := h_A }).length = p.length + 1

Tactic:
by

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴ * Aᴴᴴ = ↑(Fintype.card n) • 1

Tactic:
by

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴᴴ * Aᴴ = ↑(Fintype.card n) • 1

Tactic:
by

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Aᴴ.IsHadamard

Tactic:
by

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : Aᴴ.IsHadamard
⊢ A.IsHadamard

Tactic:
by

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
e₁ e₂ : n ≃ m
hA : A.IsHadamard
⊢ ((Matrix.reindex e₁ e₂) A).IsHadamard

Tactic:
by

Goal state after: