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

State before:
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
η : A
hη : η ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) η = 1
Tactic:
obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2).1 hη) n.2
State after:
case intro.intro
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hη : ζ ^ i ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) (ζ ^ i) = 1

State before:
case intro.intro
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hη : ζ ^ i ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) (ζ ^ i) = 1
Tactic:
rw [map_pow, ← Ideal.Quotient.algebraMap_eq, eq_one_mod_one_sub, one_pow]
State after:
no goals