Theorem: surjective_of_isCyclotomicExtension_two (FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
⊢ Function.Surjective ⇑(algebraMap R S)
Tactic:
intro x
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
⊢ ∃ a, (algebraMap R S) a = x

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
have := IsCyclotomicExtension.adjoin_roots (S := {2}) (A := R) (B := S) x
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | ∃ n ∈ {2}, b ^ ↑n = 1}
⊢ ∃ a, (algebraMap R S) a = x

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | ∃ n ∈ {2}, b ^ ↑n = 1}
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, sq_eq_one_iff, PNat.coe_two] at this
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ ∃ a, (algebraMap R S) a = x

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
H : Algebra.adjoin R {b | b = 1 ∨ b = -1} ≤ ⊥
⊢ ∃ a, (algebraMap R S) a = x
Tactic:
exact H this
State after:
no goals

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ Algebra.adjoin R {b | b = 1 ∨ b = -1} ≤ ⊥
Tactic:
rw [Algebra.adjoin_le_iff]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ {b | b = 1 ∨ b = -1} ⊆ ↑⊥

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ {b | b = 1 ∨ b = -1} ⊆ ↑⊥
Tactic:
rintro _ (rfl|rfl)
State after:
case inl
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ 1 ∈ ↑⊥

case inr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ -1 ∈ ↑⊥

State before:
case inl
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ 1 ∈ ↑⊥
Tactic:
exact one_mem _
State after:
no goals

State before:
case inr
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ -1 ∈ ↑⊥
Tactic:
exact neg_mem (one_mem _)
State after:
no goals