Pythagorean triples

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Alec Barreto and Egbert Rijke.

Created on 2022-06-30.
Last modified on 2023-09-24.

module elementary-number-theory.pythagorean-triples where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.squares-natural-numbers

open import foundation.identity-types
open import foundation.universe-levels

Idea

A Pythagorean triple is a triple (a,b,c) of natural numbers such that a² + b² = c².

Definition

is-pythagorean-triple : ℕ → ℕ → ℕ → UU lzero
is-pythagorean-triple a b c = ((square-ℕ a) +ℕ (square-ℕ b) ＝ square-ℕ c)

Recent changes