Theorem: FltRegular.is_principal (FltRegular/CaseI/Statement.lean)

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
haveI := CyclotomicField.isCyclotomicExtension P ℚ
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
replace hζ := hζ.mem_nthRootsFinset hpri.out.pos
State after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨I, hI⟩ := exists_ideal hp5 H hgcd caseI hζ
State after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

State before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
apply is_principal_aux
State after:
case intro.hreg
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))

case intro.hI
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ span {↑a + ζ * ↑b} = ?intro.I ^ p

case intro.I
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))

State before:
case intro.hreg
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))
Tactic:
rwa [IsRegularPrime, IsRegularNumber] at hreg
State after:
no goals

State before:
case intro.hI
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ span {↑a + ζ * ↑b} = ?intro.I ^ p
Tactic:
exact hI
State after:
no goals