-- Mathlib/FieldTheory/Minpoly/Field.lean
/-- The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`. -/
lemma minpoly_algHom_toLinearMap (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) :
    minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1

Proof state:
case hσ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ IsOfFinOrder ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)

Tactic:
rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = minpoly K ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

Tactic:
apply congr_arg

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ σ.toLinearMap = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

Proof state:
case h.h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
x✝ : L
⊢ σ.toLinearMap x✝ = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap x✝

Tactic:
simp

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)

Tactic:
rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]

Result:
case hf
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ Injective ⇑↑(AlgEquiv.algHomUnitsEquiv K L)

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = X ^ orderOf σ - C 1

Tactic:
rw [this, ← minpoly_algEquiv_toLinearMap]

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = minpoly K ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

case hσ
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ IsOfFinOrder ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ σ.toLinearMap = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap

Tactic:
ext

Result:
case h.h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
x✝ : L
⊢ σ.toLinearMap x✝ = ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit).toLinearMap x✝

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ minpoly K σ.toLinearMap = X ^ orderOf σ - C 1

Tactic:
have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by
  rw [← MonoidHom.coe_coe, orderOf_injective, ← orderOf_units, IsOfFinOrder.val_unit]
  exact (AlgEquiv.algHomUnitsEquiv K L).injective

Result:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
this : orderOf σ = orderOf ((AlgEquiv.algHomUnitsEquiv K L) hσ.unit)
⊢ minpoly K σ.toLinearMap = X ^ orderOf σ - C 1

Proof state:
case hf
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
σ : L →ₐ[K] L
hσ : IsOfFinOrder σ
⊢ Injective ⇑↑(AlgEquiv.algHomUnitsEquiv K L)

Tactic:
exact (AlgEquiv.algHomUnitsEquiv K L).injective

Result:
no goals