Project-declaredLean 4.33.0-rc1 · mathlib@3bc2a180

Dvd card class Group of unramified is Cyclic

dvd_card_classGroup_of_unramified_isCyclic

number theory cyclotomic fields Fermat's Last Theorem hilbert94

Plain-language statement

This is the second part of Hilbert Theorem 94, which states that if L/K is an unramified cyclic finite extension of number fields of odd prime degree, then the degree divides the class number of K.

Exact Lean statement

theorem dvd_card_classGroup_of_unramified_isCyclic {K L : Type}
    [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] [Algebra.Unramified (𝓞 K) (𝓞 L)]
    [IsCyclic (L ≃ₐ[K] L)]
    (hKL : Nat.Prime (finrank K L))
    (hKL' : finrank K L ≠ 2) :
    finrank K L ∣ Fintype.card (ClassGroup (𝓞 K))

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem dvd_card_classGroup_of_unramified_isCyclic {K L : Type}    [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]    [FiniteDimensional K L] [IsGalois K L] [Algebra.Unramified (𝓞 K) (𝓞 L)]    [IsCyclic (L ≃ₐ[K] L)]    (hKL : Nat.Prime (finrank K L))    (hKL' : finrank K L ≠ 2) :    finrank K L ∣ Fintype.card (ClassGroup (𝓞 K)) := by  obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL hKL'  have := Fact.mk hKL  rw [hKL.dvd_iff_not_coprime]  exact fun h ↦ hI (Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime h    (Ideal.isPrincipal_pow_finrank_of_isPrincipal_map hI'))

Project: FLT for regular primes
License: Apache-2.0
Commit: 1741c80894f4
Source: FltRegular/NumberTheory/Hilbert94.lean:134-145

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.33.0-rc1

Eq pow prime of unit of congruent

eq_pow_prime_of_unit_of_congruent

Plain-language statement

A regular prime criterion: if a unit of the cyclotomic field is congruent to an integer modulo p, then it is a p-th power.

number theorycyclotomic fieldsFermat's Last Theorem

Source project: FLT for regular primes

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Case I easier

FltRegular.caseI_easier

Plain-language statement

Case I with additional assumptions.

number theorycyclotomic fieldsFermat's Last Theorem

Source project: FLT for regular primes

Person-level attribution pending.

View proof record

Project-declaredLean 4.33.0-rc1

Case II

FltRegular.caseII

Plain-language statement

Case II of Fermat's Last Theorem for regular primes.

number theorycyclotomic fieldsFermat's Last Theorem

Source project: FLT for regular primes

Person-level attribution pending.

View proof record