Theorem: div_zeta_sub_one_Bijective (FltRegular/CaseII/InductionStep.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
haveI : Fact (Nat.Prime p) := hpri
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this : Fact (↑p).Prime
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this : Fact (↑p).Prime
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
letI := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime
this : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime
this : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
letI := IsCyclotomicExtension.numberField {p} ℚ K
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Function.Bijective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)
Tactic:
rw [Fintype.bijective_iff_injective_and_card]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) ∧
    Fintype.card { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } = Fintype.card (𝓞 K ⧸ 𝔭)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (Function.Injective fun η => (Ideal.Quotient.mk 𝔭) (div_zeta_sub_one hp hζ e η)) ∧
    Fintype.card { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } = Fintype.card (𝓞 K ⧸ 𝔭)
Tactic:
use div_zeta_sub_one_Injective hp hζ e hy
State after:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Fintype.card { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } = Fintype.card (𝓞 K ⧸ 𝔭)

State before:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ Fintype.card { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } = Fintype.card (𝓞 K ⧸ 𝔭)
Tactic:
simp only [PNat.pos, mem_nthRootsFinset, Fintype.card_coe]
State after:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (nthRootsFinset (↑p) (𝓞 K)).card = Fintype.card (𝓞 K ⧸ 𝔭)

State before:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (nthRootsFinset (↑p) (𝓞 K)).card = Fintype.card (𝓞 K ⧸ 𝔭)
Tactic:
rw [hζ.unit'_coe.card_nthRootsFinset, ← Submodule.cardQuot_apply, ← Ideal.absNorm_apply,
  Ideal.absNorm_span_singleton, norm_Int_zeta_sub_one hζ hp]
State after:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑p = (↑↑p).natAbs

State before:
case right
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝¹ : Fact (↑p).Prime
this✝ : Fintype (𝓞 K ⧸ 𝔭) := Fintype.ofFinite (𝓞 K ⧸ 𝔭)
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ ↑p = (↑↑p).natAbs
Tactic:
rfl
State after:
no goals