mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
⊢ ∃ a ∈ N, a ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
⊢ t_inv * t = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
⊢ toLaurentAlg M.charpoly = p

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
⊢ toLaurentAlg M.charpolyRev = q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
⊢ Function.Injective ⇑f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
A' : Subalgebra R A :=
  { carrier := {x | ∀ n ∈ N, x • n ∈ N}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯,
    algebraMap_mem' := ⋯ }
f : ↥A' →ₐ[R] Module.End R ↥N :=
  AlgHom.ofLinearMap { toFun := fun x ↦ (DistribSMul.toLinearMap R M x).restrict ⋯, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
a : M
ha₁ : a ∈ N
ha₂ : a ≠ 0
this : Function.Injective ⇑f
⊢ Module.Finite R ↥N

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.charpoly.reverse = M.charpolyRev

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ ((scalar n) X - C.mapMatrix A⁻¹).det = C (A⁻¹ * A).det * ((scalar n) X - C.mapMatrix A⁻¹).det

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C (A⁻¹ * A).det * ((scalar n) X - C.mapMatrix A⁻¹).det = C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det =
    C A⁻¹.det * (C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : IsDomain A
M : Type u_5
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : Module.IsTorsionFree A M
N : Submodule R M
hN : N ≠ ⊥
hN' : N.FG
x : A
hx : ∀ n ∈ N, x • n ∈ N
⊢ IsIntegral R x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det) =
    C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y z : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
hz : z ∈ Subring.closure {x, y}
⊢ f.IsIntegralElem z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x y : S
hx : f.IsIntegralElem x
hy : f.IsIntegralElem y
⊢ f.IsIntegralElem (x - y)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 0 ≤ #s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: B : Type u_3
S : Type u_4
inst✝⁶ : Ring B
inst✝⁵ : CommRing S
R : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Algebra R B
inst✝² : Algebra S B
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S B
x : B
r : R
hx : IsIntegral S x
⊢ r • x ∈ S[x]

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ 0 < #s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
⊢ 0 ≤ Fintype.card α

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
⊢ 0 ≤ s.dens

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
⊢ 0 < s.dens

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
⊢ s.dens ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
n : ℤ
⊢ IsIntegral R ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < #univ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
a : ℕ
⊢ IsIntegral R ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < Fintype.card α

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ 0 < univ.dens

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ univ.dens ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Positivity.Finset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Fintype α
G : Type u_2
A : Finset G
⊢ let f := fun x ↦ 1;
  (∀ (s : G), f s ^ 2 = 1) → 0 ≤ #A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x ⊗ₜ[R] y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g h : G
x : ↥(integralClosure R K)
⊢ (g * h) • x = g • h • x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det =
    C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
x : ↥(integralClosure R K)
⊢ 1 • x = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ g • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x + y) = g • x + g • y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x + y) = g • x + g • y

Tactic:
by ext; exact smul_add g (x : K) (y : K)

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
⊢ g • 1 = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * A.charpolyRev

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ g • (x * y) = g • x * g • y

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
⊢ A⁻¹.charpoly = (-1) ^ Fintype.card n * C A.det⁻¹ʳ * A.charpolyRev

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 - X • M.map ⇑C).map (eval 0) = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ eval 0 M.charpolyRev = 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : M ^ k = 0
⊢ 1 - X • M.map ⇑C ∣ 1

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ IsUnit M.charpolyRev

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
this : IsNilpotent (M.charpolyRev.coeff 1)
⊢ IsNilpotent M.trace

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ IsNilpotent M.trace

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
⊢ p - 1 = X * (p /ₘ X)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
⊢ max M.charpoly.natDegree (X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (hasseDeriv k) f = f.sum fun i r ↦ (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ IsNilpotent (M.charpoly - X ^ Fintype.card n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ ((hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 0) f = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (hasseDeriv n) p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 1) f = derivative f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
⊢ (hasseDeriv k) ((monomial n) r) = (monomial (n - k)) (↑(n.choose k) * r)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) (C r) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 0 < k
⊢ (hasseDeriv k) 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
hk : 1 < k
⊢ (hasseDeriv k) X = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
⊢ A.submatrix ⇑e ⇑e = fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ n + k + 1 = n + (k + 1)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
⊢ (of (s.piecewise M.row (row 1))).det = (M.submatrix Subtype.val Subtype.val).det

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
⊢ ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
⊢ ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l : ℕ
⊢ hasseDeriv k ∘ₗ hasseDeriv l = (k + l).choose k • hasseDeriv (k + l)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
s : Finset n
n✝ : ℕ
⊢ (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i) = fun i ↦
    (if i ∈ s then X else 1) • s.piecewise (fun i ↦ M.map (⇑C) i) (fun i ↦ 1 i) i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r✝ : R
f✝ : R[X]
r c : R
f : R[X]
⊢ (c • f).comp (X + C r) = (RingHom.id R) c • f.comp (X + C r)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (taylor 0) f = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
i : ℕ
k : R
⊢ (taylor r) ((monomial i) k) = C k * (X + C r) ^ i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff 0 = eval r f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff 1 = eval r (derivative f)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree ≤ p.natDegree - n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).natDegree = p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv f.natDegree) f = C f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ((taylor r) f).leadingCoeff = f.leadingCoeff

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ((hasseDeriv n) p).natDegree = p.natDegree - n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ (taylor r) f = 0 ↔ f = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
h_det : ∀ (s : Finset n), D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = C (det (s.piecewise M 1))
⊢ (∑ s, D (s.piecewise (fun i ↦ (X • M.map ⇑C) i) fun i ↦ 1 i)).coeff k =
    (∑ s, X ^ #s • D (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i)).coeff k

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).degree = p.degree

Tactic:
by

Goal state after: