def FltRegular.Statement : Prop

Statement of Fermat's last theorem for regular primes.

Equations

• FltRegular.Statement = ∀ ⦃p : ℕ⦄ [inst : Fact (Nat.Prime p)], IsRegularPrime p → p ≠ 2 → FermatLastTheoremWith ℤ p

theorem flt_regular {p : ℕ} [Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (hodd : p ≠ 2) : FermatLastTheoremWith ℤ p

Fermat's last theorem for regular primes.