mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ (toFunAlgHom n R A) (invFun n R A M) = M

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
⊢ (fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A) M) = M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.1 ∧ j = p.2 ↔ p = (i, j)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ (matrixEquivTensor n R A) (single i j x) = x ⊗ₜ[R] single i j 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Semiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ (kroneckerTMulAlgEquiv m n R S A B) (star 0) = star ((kroneckerTMulAlgEquiv m n R S A B) 0)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Semiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x : Matrix m m A) (y : Matrix n n B),
    (kroneckerTMulAlgEquiv m n R S A B) (star (x ⊗ₜ[R] y)) = star ((kroneckerTMulAlgEquiv m n R S A B) (x ⊗ₜ[R] y))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
⊢ X ^ Fintype.card n * (A * B).charpoly = X ^ Fintype.card m * (B * A).charpoly

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Semiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ ∀ (x y : Matrix m m A ⊗[R] Matrix n n B),
    (kroneckerTMulAlgEquiv m n R S A B) (star x) = star ((kroneckerTMulAlgEquiv m n R S A B) x) →
      (kroneckerTMulAlgEquiv m n R S A B) (star y) = star ((kroneckerTMulAlgEquiv m n R S A B) y) →
        (kroneckerTMulAlgEquiv m n R S A B) (star (x + y)) = star ((kroneckerTMulAlgEquiv m n R S A B) (x + y))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ (kroneckerAlgEquiv m n R) (star 0) = star ((kroneckerAlgEquiv m n R) 0)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x : Matrix m m R) (y : Matrix n n R),
    (kroneckerAlgEquiv m n R) (star (x ⊗ₜ[R] y)) = star ((kroneckerAlgEquiv m n R) (x ⊗ₜ[R] y))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ ∀ (x y : Matrix m m R ⊗[R] Matrix n n R),
    (kroneckerAlgEquiv m n R) (star x) = star ((kroneckerAlgEquiv m n R) x) →
      (kroneckerAlgEquiv m n R) (star y) = star ((kroneckerAlgEquiv m n R) y) →
        (kroneckerAlgEquiv m n R) (star (x + y)) = star ((kroneckerAlgEquiv m n R) (x + y))

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
hle : Fintype.card n ≤ Fintype.card m
⊢ (A * B).charpoly = X ^ (Fintype.card m - Fintype.card n) * (B * A).charpoly

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
⊢ a ≤ d

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Ring.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b c d : α
h1 : a = b
h2 : b < c
h3 : d = c
⊢ a < d

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ (↑M * N * (↑M)⁻¹).charpoly = N.charpoly

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * N * ↑M).charpoly = N.charpoly

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
μ : R
⊢ (M - (scalar n) μ).charpoly = M.charpoly.comp (X + C μ)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (A - B * ⅟D * C)
⊢ Invertible (fromBlocks A B C D)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (D - C * ⅟A * B)
⊢ Invertible (fromBlocks A B C D)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible (D - C * ⅟A * B)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟A + ⅟A * B * ⅟(D - C * ⅟A * B) * C * ⅟A) (-(⅟A * B * ⅟(D - C * ⅟A * B)))
      (-(⅟(D - C * ⅟A * B) * C * ⅟A)) ⅟(D - C * ⅟A * B)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
⊢ Invertible (A - B * ⅟D * C)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (A - B * ⅟D * C)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (fromBlocks A B C D)
⊢ Invertible (D - C * ⅟A * B)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟A * B)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ (fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks 1 B C D).det = (D - C * B).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 0 = x ^ 0 + ↑0 * x ^ (0 - 1) * y + 0 * y ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 1 = x ^ 1 + ↑1 * x ^ (1 - 1) * y + 0 * y ^ 2

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ (fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
det_fromBlocks₂₂,

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
this : Invertible 1
⊢ det 1 * (A - B * ⅟1 * C).det = (A - B * C).det
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 + A * B).det = (fromBlocks 1 (-A) B 1).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x + y) ^ (n + 1) = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2)

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (A * B + 1).det = (B * A + 1).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - A * B).det = (1 - B * A).det

Tactic:
by

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

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u

Tactic:
by

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

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n✝ : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
n : ℕ
⊢ { k // (x + y) ^ (n + 2) = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 2 - 1) * y + k * y ^ 2 }

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
U : Matrix m n α
V : Matrix n m α
hA : IsUnit A.det
⊢ (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : CommRing R
x y : R
e : ℕ
a : R
⊢ { k // a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + k * y ^ 2) }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = f.sum fun e a ↦ a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(polyBinomAux1 x y e a) * y ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f =
    ((f.sum fun e a ↦ a * x ^ e) + f.sum fun e a ↦ a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a ↦ a * ↑(polyBinomAux1 x y e a) * y ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ { k // eval (x + y) f = eval x f + eval x (derivative f) * y + k * y ^ 2 }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 0 - y ^ 0 = 0 * (x - y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 1 - y ^ 1 = 1 * (x - y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x : R
inst✝ : Ring R
h : IsNilpotent x
⊢ IsNilpotent (-x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k✝ : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
k : ℕ
⊢ { z // x ^ (k + 2) - y ^ (k + 2) = z * (x - y) }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ ¬IsNilpotent (-1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
⊢ (-1) ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ { z // eval x f - eval y f = z * (x - y) }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
inst✝² : MulActionWithZero R S
inst✝¹ : SMulCommClass R S S
inst✝ : IsScalarTower R S S
a : S
ha : IsNilpotent a
t : R
⊢ IsNilpotent (t • a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (1 - r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r + 1)

Tactic:
by

Goal state after: