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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ LinearMap.det ((lmul R S) ((algebraMap R S) x)) = x ^ Fintype.card ι

Tactic:
← det_toMatrix b,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ((toMatrix b b) ((lmul R S) ((algebraMap R S) x))).det = x ^ Fintype.card ι
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type w
inst✝ : Fintype ι
b : Basis ι R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ Fintype.card ι

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Free R S
x : R
⊢ (norm R) ((algebraMap R S) x) = x ^ finrank R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Free R S
n : ℕ
⊢ (norm R) ↑n = ↑n ^ finrank R S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n = (of (X ^ n - C a)) a

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : 1 < n
a : K
⊢ X.natDegree < (X ^ n - C a).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ (C a).natDegree < (X - C a).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
hn : 0 < n
ha : a ≠ 0
⊢ root (X ^ n - C a) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hn : n ≠ 1
a : K
H : Irreducible (X ^ n - C a)
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
e : n = 0
⊢ Irreducible (C (1 - a))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible ((X ^ k - C b) * q)
hq : (X ^ k) ^ m - C b ^ m = (X ^ k - C b) * q
⊢ q.degree = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse
    (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) fun i ↦
      (Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ⇑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
⊢ b ^ m ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬(0 * 0 ∣ 0 → IsUnit 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ ¬Squarefree 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
m : R
hm : Squarefree m
⊢ m ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
⊢ Squarefree x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ 2 ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
⊢ n = 0 ∨ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
⊢ x ^ n ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬IsUnit (X ^ p - C a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r a : R
⊢ ¬IsMax 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoid R
r : R
⊢ Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0
⊢ 0 = 0 ∧ ∀ (x : R), ¬Irreducible x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : r ≠ 0
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
⊢ x ∣ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ (z * w) ^ 2 = z * z * w * w

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x : R
h0 : x ≠ 0
h : IsRadical x
⊢ Squarefree x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
y p : R
k : ℕ
hp : Prime p
x' : R
hx : Squarefree (p * x')
h : p ^ (k + 1) ∣ p * x' * y
hx' : ¬p ∣ x'
⊢ p ^ k ∣ x' * y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y p : R
k : ℕ
hx : Squarefree x
hp : Prime p
h : p ^ (k + 1) ∣ x * y
⊢ p ^ k ∣ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsCancelMulZero R
x y p : R
k : ℕ
hy : Squarefree y
hp : Prime p
h : p ^ (k + 1) ∣ x * y
⊢ p ^ k ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
eq : d * d = a * b
ha : Squarefree a
⊢ d ^ 2 = a * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
a✝ : Nontrivial R
a b : R
hb : b ∣ y
ha : Squarefree a
c : R
eq : c * (a * c) = b
hc : d = a * c
⊢ b = d * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x y d : R
inst✝ : DecompositionMonoid R
hx : Squarefree x
h : d * d ∣ x * y
⊢ d ∣ y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ a ∈ cons a s ha

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
i : ι
hi : i ∈ s
⊢ i ∈ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
s : Finset ι
f : ι → R
hs : (↑s).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ s, Squarefree (f i)
⊢ Squarefree (∏ i ∈ s, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
x : R
inst✝ : DecompositionMonoid R
⊢ x = 0 → IsRadical x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (X ^ p - C a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
z p : R
hz : z ≠ 0
hp : Irreducible p
ih : z ≠ 0 → ∃ y n, Squarefree y ∧ y ∣ z ∧ z ∣ y ^ n
hx : p * z ≠ 0
y : R
hy : Squarefree y
hyx : y ∣ z
hy' : z ∣ y ^ 0
⊢ p * z ∣ p ^ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
x : R
hx : x ≠ 0
⊢ ∃ y n, Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ ¬Separable 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : R[X]
⊢ f.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a : R
⊢ (X + C a).Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
⊢ (C r).Separable ↔ IsUnit r

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ f.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ g.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
⊢ g.Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ IsCoprime f g

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 2)).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ Squarefree x ↔ (normalizedFactors x).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + b * derivative p = 1
⊢ Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * derivative (Polynomial.map f p) = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R[X]
ha : Associated f g
h : f.Separable
⊢ g.Separable

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: n : ℤ
⊢ Squarefree n.natAbs ↔ Squarefree n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
⊢ eval₂ f x (derivative p) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: n : ℕ
⊢ Squarefree ↑n ↔ Squarefree n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * (q * p)) (q * (derivative q * p + derivative q * p + q * derivative p))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hp : p.Separable
hq : q * q ∣ p
⊢ IsUnit q

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
⊢ emultiplicity q p ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ Squarefree p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : R
⊢ (X - C x).Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝² : CommRing A
n : Type u_7
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M N : Matrix n n A
⊢ (M * N).det = (N * M).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ x ∈ insert a s, (f x).Separable
⊢ (∏ x ∈ insert a s, f x).Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : (∏ i ∈ s, (X - C (f i))).Separable
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N).det = (N * M).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ s.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
⊢ (X ^ n - C ↑u).Separable

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
u : Rˣ
a✝ : Nontrivial R
hn : IsUnit ↑0
⊢ (X ^ 0 - C ↑u).Separable

case inr
R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
⊢ (X ^ n - C ↑u).Separable
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N * M').det = N.det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
    C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1))

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
a✝ : Nontrivial R
hpos : n > 0
n' : R
hn' : n' * ↑n = 1
⊢ C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
u : Rˣ
hn : IsUnit ↑n
⊢ (X ^ n - C ↑u).Separable

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
⊢ derivative f = C b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_6
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ ((toMatrix b b) f).det = ((toMatrix c c) f).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb : IsUnit b
⊢ (C a * X ^ n + C b * X + C c).Separable

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ (detAux (Trunc.mk b)) f = ((toMatrix b b) f).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ Multiset.count x p.roots ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hsep : p.Separable
⊢ p.roots.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
ι' : Type u_7
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ (detAux tb) f = ((toMatrix b' b') f).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : Irreducible f
h : derivative f ≠ 0
g : F[X]
hg1 : g ∈ nonunits F[X]
_hg2 : g ≠ 0
x✝ : g ∣ f
hg4 : g ∣ derivative f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : ↑u = p
⊢ f ∣ derivative f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
⊢ ⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : LinearMap.det f ≠ 1
⊢ Free R M

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ i ∈ s, (X - C (f i))).Separable

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ x ∈ univ, ∀ y ∈ univ, f x = f y → x = y) ↔ Function.Injective f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ ((toMatrix b b) f).det = LinearMap.det f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: A : Type u_5
inst✝² : CommRing A
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : (ι → A) →ₗ[A] ι → A
⊢ (toMatrix' f).det = LinearMap.det f

Tactic:
by

Goal state after: