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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ Function.Injective ⇑(of f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ Module.End.IsSemisimple (LinearMap.mulRight K a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ AdjoinRoot f →+* S

Tactic:
apply Ideal.Quotient.lift _ (eval₂RingHom i x)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ ∀ a ∈ span {f}, (eval₂RingHom i x) a = 0
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
M' : Type u_3
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
⊢ M ≃ₗ[R] M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Lie.AdjointAction.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : Field K
inst✝³ : PerfectField K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
⊢ ((ad K (Module.End K V)) a).IsSemisimple

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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
x : M
⊢ (equivOfIsUnitDet h) x = f x

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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
⊢ ↑(equivOfIsUnitDet h) = f

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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit (LinearMap.det f)
⊢ ↑(equivOfIsUnitDet h) = f

Tactic:
by
  ext
  apply LinearMap.equivOfIsUnitDet_apply

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
⊢ AdjoinRoot f →+* S

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✝
M' : Type u_3
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M✝
𝕜 : Type u_5
inst✝³ : Field 𝕜
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 0
⊢ IsUnit ((toMatrix (finBasis 𝕜 M) (finBasis 𝕜 M)) f).det

Tactic:
rw [LinearMap.det_toMatrix]

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M✝ : Type u_2
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
M' : Type u_3
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M✝
𝕜 : Type u_5
inst✝³ : Field 𝕜
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 0
⊢ IsUnit (LinearMap.det f)
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ (lift i a h) (root f) = a

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✝
M' : Type u_3
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M✝
𝕜 : Type u_5
inst✝³ : Field 𝕜
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 0
⊢ IsUnit ((toMatrix (finBasis 𝕜 M) (finBasis 𝕜 M)) f).det

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ (lift i a h) ((of f) x) = i x

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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
this : Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f')
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
f g : R[X]
inst✝³ : CommRing S
i✝ : R →+* S
a : S
h✝ : eval₂ i✝ a f = 0
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
r : S
⊢ (↑↑(lift i.toRingHom x h)).toFun ((algebraMap S (AdjoinRoot p)) r) = (algebraMap S T) r

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
r : R
⊢ (liftAlgHom p i x h) ((of p) r) = i r

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
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), f x = f' (e x)
⊢ Associated (LinearMap.det f) (LinearMap.det f')

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S R
inst✝ : Algebra S T
p : R[X]
i : R →ₐ[S] T
x : T
h : eval₂ (↑i) x p = 0
⊢ (liftAlgHom p i x h) (root p) = x

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
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ (aeval (ϕ (root f))) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
f : R[X]
inst✝¹ : CommRing S
inst✝ : Algebra R S
ϕ : AdjoinRoot f →ₐ[R] S
⊢ liftAlgHom f (Algebra.ofId R S) (ϕ (root f)) ⋯ = ϕ

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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
i : ι
x y : M
⊢ (e.toMatrix (update v i (x + y))).det = (e.toMatrix (update v i x)).det + (e.toMatrix (update v i y)).det

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
⊢ (of (C r * X - 1)) r * root (C r * X - 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ (algebraMap R S) r * f (root (C r * X - 1)) = 1

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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
u : ι → M
i : ι
c : R
x : M
⊢ (e.toMatrix (update u i (c • x))).det = c • (e.toMatrix (update u i x)).det

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ (algebraMap R S) r * g (root (C r * X - 1)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
⊢ eval₂ ((of q).comp f) (root q) p = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
r : R
⊢ (map f p q h) ((of p) r) = (of q) (f r)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
p : R[X]
q : S[X]
h : q ∣ Polynomial.map f p
⊢ (map f p q h) (root p) = root q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ Polynomial.map g q ∣ Polynomial.map (g.comp f) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
p : R[X]
q : S[X]
r : T[X]
hf : q ∣ Polynomial.map f p
hg : r ∣ Polynomial.map g q
⊢ (map g q r hg).comp (map f p q hf) = map (g.comp f) p r ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ p ∣ Polynomial.map (↑f.symm) q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ (map (↑f) p q ⋯).comp (map (↑f.symm) q p ⋯) = RingHom.id (AdjoinRoot q)

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
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → (MultilinearMap.mk' (fun v ↦ (e.toMatrix v).det) ⋯ ⋯).toFun v = 0

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ e.det ⇑e = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ (map (↑f.symm) q p ⋯).comp (map (↑f) p q ⋯) = RingHom.id (AdjoinRoot p)

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
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : IsEmpty ι
⊢ e.det = AlternatingMap.constOfIsEmpty R M ι 1

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
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : Nontrivial R
h : e.det = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝² : CommRing R
f✝ g : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝ : CommRing T
f : R ≃+* S
p : R[X]
q : S[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ Associated (Polynomial.map (↑f.symm) q) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
p : S[X]
q : T[X]
h : q ∣ Polynomial.map (↑f) p
r : R
⊢ (↑↑(map (↑f) p q h)).toFun ((algebraMap R (AdjoinRoot p)) r) = (algebraMap R (AdjoinRoot q)) r

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
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
g : G
v : ι → M
⊢ (g • e).det v = e.det (g⁻¹ • v)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f) p
hg : r ∣ Polynomial.map (↑g) q
⊢ Polynomial.map (↑g) q ∣ Polynomial.map (↑(g.comp f)) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S →ₐ[R] T
g : T →ₐ[R] U
p : S[X]
q : T[X]
r : U[X]
hf : q ∣ Polynomial.map (↑f) p
hg : r ∣ Polynomial.map (↑g) q
⊢ (mapAlgHom g q r hg).comp (mapAlgHom f p q hf) = mapAlgHom (g.comp f) p r ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ (↑f.toRingEquiv.symm).comp ↑f = RingHom.id S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ p ∣ Polynomial.map (↑↑f.symm) q

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
h : IsUnit ((LinearMap.toMatrix e e) ((e.constr ℕ) v)).det
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ ⇑v' = v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ (mapAlgHom (↑f) p q ⋯).comp (mapAlgHom (↑f.symm) q p ⋯) = AlgHom.id R (AdjoinRoot q)

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
v : ι → M
⊢ LinearIndependent R v ∧ span R (Set.range v) = ⊤ ↔ IsUnit (e.det v)

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
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
⊢ f = f ⇑e • e.det

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
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ (mapAlgHom (↑f.symm) q p ⋯).comp (mapAlgHom (↑f) p q ⋯) = AlgHom.id R (AdjoinRoot p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ Associated (Polynomial.map (↑f.symm) q) p

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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
⊢ e.det (⇑f ∘ v) = LinearMap.det f * e.det v

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f g : S[X]
hgf : g ∣ f
⊢ g ∣ Polynomial.map (↑(AlgHom.id R S)) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f g : S[X]
hgf : g ∣ f
⊢ (mk g) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hgf : g ∣ f
⊢ (algHomOfDvd R f g hgf) (root f) = root g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f g : S[X]
hfg : Associated f g
⊢ Associated (Polynomial.map (↑AlgEquiv.refl) f) g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hfg : Associated f g
⊢ (algEquivOfAssociated R f g hfg) (root f) = root g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝⁶ : CommRing R
f✝ g✝ : R[X]
inst✝⁵ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f g : S[X]
hfg : f = g
⊢ Associated f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f g : S[X]
hfg : f = g
⊢ (algEquivOfEq R f g hfg) (root f) = root g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by
    rw [← map_natCast (of f), ← map_natCast (of f), ← map_div₀, ← NNRat.cast_def]; rfl

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 b' b'' : Basis ι A M
⊢ ⇑b'' = ⇑↑(b'.equiv b'' (Equiv.refl ι)) ∘ ⇑b'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ≥0
x : AdjoinRoot f
p : K[X]
⊢ q • (mk f) p = (of f) ↑q * (mk f) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : Field K
f : K[X]
inst✝ : Fact (Irreducible f)
q : ℚ
x : AdjoinRoot f
p : K[X]
⊢ q • (mk f) p = (of f) ↑q * (mk f) p

Tactic:
by

Goal state after: