-- Mathlib/NumberTheory/NumberField/Norm.lean
theorem isUnit_norm [CharZero K] {x : 𝓞 F} : IsUnit (norm K x) ↔ IsUnit x

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
letI : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K

Result:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
haveI : IsAlgClosure K (AlgebraicClosure F) :=
  IsAlgClosure.ofAlgebraic K F (AlgebraicClosure F)

Result:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsAlgClosure K (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F ↥L
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
calc
  IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) :=
    (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
  _ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
    rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
  _ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := isUnit_norm_of_isGalois K
  _ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
  _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
  _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)

Result:
no goals

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
haveI : FiniteDimensional F L := FiniteDimensional.right K F L

Result:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F ↥L
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) ((algebraMap (𝓞 F) (𝓞 ↥L)) x))

Tactic:
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]

Result:
no goals

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsAlgClosure K (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L

Result:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F ↥L
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Proof state:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
let L := normalClosure K F (AlgebraicClosure F)

Result:
K : Type u_2
inst✝⁵ : Field K
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : Algebra.IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit ((norm K) x) ↔ IsUnit x