Theorem: dvd_card_classGroup_of_isUnramified_isCyclic (FltRegular/NumberTheory/Hilbert94.lean)

State before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL hKL'
State after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))

State before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
letI := Fact.mk hKL
State after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))

State before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))
Tactic:
rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_coprime,
  Nat.isCoprime_iff_coprime]
State after:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ ¬(finrank K L).Coprime (Fintype.card (ClassGroup (𝓞 K)))

State before:
case intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝²⁵ : Field K✝
inst✝²⁴ : NumberField K✝
inst✝²³ : Fintype (ClassGroup (𝓞 K✝))
L✝ : Type ?u.157534
inst✝²² : Field L✝
inst✝²¹ : Algebra K✝ L✝
inst✝²⁰ : FiniteDimensional K✝ L✝
inst✝¹⁹ : IsGalois K✝ L✝
σ : L✝ ≃ₐ[K✝] L✝
hσ : ∀ (x : L✝ ≃ₐ[K✝] L✝), x ∈ Subgroup.zpowers σ
hKL✝ : finrank K✝ L✝ = ↑p
A : Type ?u.159425
B : Type ?u.159428
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra A L✝
inst✝¹⁴ : Algebra A K✝
inst✝¹³ : Algebra B L✝
inst✝¹² : IsScalarTower A B L✝
inst✝¹¹ : IsScalarTower A K✝ L✝
inst✝¹⁰ : IsFractionRing A K✝
inst✝⁹ : IsIntegralClosure B A L✝
K : Type u_2
L : Type u_3
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : NumberField K
inst✝⁵ : NumberField L
inst✝⁴ : Algebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsGalois K L
inst✝¹ : IsUnramified (𝓞 K) (𝓞 L)
inst✝ : IsCyclic (L ≃ₐ[K] L)
hKL : (finrank K L).Prime
hKL' : finrank K L ≠ 2
I : Ideal (𝓞 K)
hI : ¬Submodule.IsPrincipal I
hI' : Submodule.IsPrincipal (Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I)
this : Fact (finrank K L).Prime := { out := hKL }
⊢ ¬(finrank K L).Coprime (Fintype.card (ClassGroup (𝓞 K)))
Tactic:
exact fun h ↦ hI (IsPrincipal_of_IsPrincipal_pow_of_Coprime _ _ h _
  (Ideal.isPrincipal_pow_finrank_of_isPrincipal_map _ hI'))
State after:
no goals