Theorem: inv_coe_coe (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ (↑↑s)⁻¹ = ↑↑s⁻¹
Tactic:
apply inv_eq_of_mul_eq_one_right
State after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑s * ↑↑s⁻¹ = 1

State before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑s * ↑↑s⁻¹ = 1
Tactic:
change ((s * s⁻¹ : Sˣ) : K) = 1
State after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑(s * s⁻¹) = 1

State before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑(s * s⁻¹) = 1
Tactic:
rw [mul_inv_self]
State after:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑1 = 1

State before:
case a
p : ℕ+
K✝ : Type ?u.244158
inst✝⁵ : Field K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
inst✝⁴ : NumberField K✝
inst✝³ : IsCyclotomicExtension {p} ℚ K✝
K : Type u_1
A : Type u_2
inst✝² : Field K
inst✝¹ : SetLike A K
inst✝ : SubsemiringClass A K
S : A
s : (↥S)ˣ
⊢ ↑↑1 = 1
Tactic:
rfl
State after:
no goals