Theorem: IsPrimitiveRoot.unit'_coe (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
have z1 := hζ
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
have : (algebraMap R K) (hζ.unit' : R) = ζ := rfl
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ζ ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
rw [← this] at z1
State after:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑hζ.unit') ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p

State before:
p : ℕ+
K : Type u_1
inst✝¹ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝ : NumberField K
z1 : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑hζ.unit') ↑p
this : (algebraMap (𝓞 K) K) ↑hζ.unit' = ζ
⊢ IsPrimitiveRoot ↑hζ.unit' ↑p
Tactic:
exact z1.of_map_of_injective (IsFractionRing.injective _ _)
State after:
no goals