Theorem: IsUnit.eq_mul_left_iff (FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean)

State before:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ x = y * x ↔ y = 1
Tactic:
nth_rw 1 [← one_mul x]
State after:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ 1 * x = y * x ↔ y = 1

State before:
p : ℕ+
K : Type ?u.152499
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
S : Type u_1
inst✝ : CommRing S
x : S
hx : IsUnit x
y : S
⊢ 1 * x = y * x ↔ y = 1
Tactic:
rw [eq_comm, hx.mul_left_injective.eq_iff]
State after:
no goals