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

State before:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ (algebraMap A (A ⧸ Ideal.span {t - 1})) t = 1
Tactic:
rw [← map_one <| algebraMap A <| A ⧸ Ideal.span ({t - 1} : Set A), ← sub_eq_zero, ← map_sub,
  Ideal.Quotient.algebraMap_eq, Ideal.Quotient.eq_zero_iff_mem]
State after:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ Ideal.span {t - 1}

State before:
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ Ideal.span {t - 1}
Tactic:
apply Ideal.subset_span
State after:
case a
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ {t - 1}

State before:
case a
p : ℕ+
K : Type ?u.53883
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
A : Type u_1
inst✝ : CommRing A
t : A
⊢ t - 1 ∈ {t - 1}
Tactic:
exact Set.mem_singleton _
State after:
no goals