Mathlib.Algebra

Statements of Mathlib (commit c31114ff81), each with its Lean source, its translation to Dedukti by Export.lean, and its informalization by Informath, in English, as a formula, and in French, Czech, German and Swedish, which the buttons at each entry show there, and the check boxes above the entries everywhere. The Dedukti translation drops implicit and instance arguments and maps Lean's arithmetic and logic to Informath's base (mapping.tsv); the other Mathlib constants are worded by the symbol table mathlib.dkgf, whose English wordings Informath also renders in the other languages. Constants without a wording appear as $\mathrm{name}$.

modulestatementsfully worded, EnglishFrenchCzechGermanSwedish
Mathlib.Algebra.Group.Nat.Units444444
Mathlib.Algebra.Prime.Defs252525252424
Show also:

Mathlib.Algebra.Group.Nat.Units source

Nat.units_eq_onetheoremUnits.lean:24
Lean
lemma units_eq_one (u : ℕˣ) : u = 1 := Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩
Dedukti
2 lines
def Nat__units_eq_one : (u : Elem (Units Nat)) -> Proof (Eqt (Units Nat) u 1) :=
  u => Units__ext Nat u 1 (Nat__eq_one_of_dvd_one (Units__val u) (existsI Nat (c => Eq 1 (times (Units__val u) c)) (Units__inv u) (Eq__symm Nat (times (Units__val u) (Units__inv u)) 1 (Units__val_inv Nat u)))).
English
Let $u$ be a unit of $\Natural$. Then $\EqtMACRoH {u}{1}$.
French
Soit $u$ une unité de $\Natural$. Alors $u$ est égal à $1$.
Czech
Nechť $u$ je jednotka $\Natural$. Tedy $\EqtMACRoH {u}{1}$.
German
Sei $u$ eine Einheit von $\Natural$. Dann $\EqtMACRoH {u}{1}$.
Swedish
Låt $u$ vara en enhet av $\Natural$. Då $\EqtMACRoH {u}{1}$.
Formula
$u \in \UnitsMACRoAX {\Natural}\vdash \EqtMACRoJ {u}{1}$
Proof
6 lines
1.Let $u$ be an element of $\UnitsMACRoAX {\Natural}$.
2.The product of the underlying value in the base of $u$ and the inverse of $u$ is equal to $1$.Units.val_inv
3.$1$ is equal to the product of the underlying value in the base of $u$ and the inverse of $u$.Eq.symm 2
4.There exists an element $c$ of $\Natural$, such that $1$ is equal to the product of the underlying value in the base of $u$ and $c$.existsI 3
5.The underlying value in the base of $u$ is equal to $1$.Nat.eq_one_of_dvd_one 4
6.$\EqtMACRoJ {u}{1}$.Units.ext 5
Proof, French
6 lines
1.Soit $u$ un élément de $\UnitsMACRoAX {\Natural}$.
2.Le produit du [DepNoun] sous-jacent de $u$ et de l'inverse de $u$ est égal à $1$.Units.val_inv
3.$1$ est égal au produit du [DepNoun] sous-jacent de $u$ et de l'inverse de $u$.Eq.symm 2
4.Il existe un élément $c$ de $\Natural$ tel que $1$ soit égal au produit du [DepNoun] sous-jacent de $u$ et de $c$.existsI 3
5.Le [DepNoun] sous-jacent de $u$ est égal à $1$.Nat.eq_one_of_dvd_one 4
6.$\EqtMACRoJ {u}{1}$.Units.ext 5
Proof, Czech
6 lines
1.Nechť $u$ je prvek $\UnitsMACRoAX {\Natural}$.
2.Součin podkladového [DepNoun] $u$ a inverze $u$ je rovný do $1$.Units.val_inv
3.$1$ je rovné do součinu podkladového [DepNoun] $u$ a inverze $u$.Eq.symm 2
4.Existuje prvek $c$ $\Natural$, takový, že $1$ je rovné součinu podkladového [DepNoun] $u$ a $c$.existsI 3
5.Podkladový [DepNoun] $u$ je rovný $1$.Nat.eq_one_of_dvd_one 4
6.$\EqtMACRoJ {u}{1}$.Units.ext 5
Proof, German
6 lines
1.Sei $u$ ein Element von $\UnitsMACRoAX {\Natural}$.
2.Units.val_inv
3.Eq.symm 2
4.existsI 3
5.Nat.eq_one_of_dvd_one 4
6.$\EqtMACRoJ {u}{1}$.Units.ext 5
Proof, Swedish
6 lines
1.Låt $u$ vara ett element av $\UnitsMACRoAX {\Natural}$.
2.$\EqtMACRoJ {\operatorname{val} (u)\times \operatorname{inv} (u)}{1}$.Units.val_inv
3.$\EqtMACRoJ {1}{\operatorname{val} (u)\times \operatorname{inv} (u)}$.Eq.symm 2
4.Det finns ett element $c$ av $\Natural$, så att $1 = \operatorname{val} (u)\times c$.existsI 3
5.$\operatorname{val} (u)= 1$.Nat.eq_one_of_dvd_one 4
6.$\EqtMACRoJ {u}{1}$.Units.ext 5
Nat.addUnits_eq_zerotheoremUnits.lean:26
Lean
lemma addUnits_eq_zero (u : AddUnits ℕ) : u = 0 :=
  AddUnits.ext (Nat.eq_zero_of_add_eq_zero u.val_neg).1
Dedukti
2 lines
def Nat__addUnits_eq_zero : (u : Elem (AddUnits Nat)) -> Proof (Eqt (AddUnits Nat) u 0) :=
  u => AddUnits__ext Nat u 0 (andEl (Eq (AddUnits__val u) 0) (Eq (AddUnits__neg u) 0) (Nat__eq_zero_of_add_eq_zero (AddUnits__val u) (AddUnits__neg u) (AddUnits__val_neg Nat u))).
English
Let $u$ be an additive unit of $\Natural$. Then $\EqtMACRoH {u}{0}$.
French
Soit $u$ une unité additive de $\Natural$. Alors $u$ est égal à $0$.
Czech
Nechť $u$ je aditivní jednotka $\Natural$. Tedy $\EqtMACRoH {u}{0}$.
German
Sei $u$ eine additive Einheit von $\Natural$. Dann $\EqtMACRoH {u}{0}$.
Swedish
Låt $u$ vara en additiv enhet av $\Natural$. Då $\EqtMACRoH {u}{0}$.
Formula
$u \in \mathrm{AddUnits} (\Natural)\vdash \EqtMACRoJ {u}{0}$
Proof
5 lines
1.Let $u$ be an additive unit of $\Natural$.
2.The sum of the underlying value in the base of $u$ and the negation of $u$ is equal to $0$.AddUnits.val_neg
3.The underlying value in the base of $u$ is equal to $0$ and the negation of $u$ is equal to $0$.Nat.eq_zero_of_add_eq_zero 2
4.The underlying value in the base of $u$ is equal to $0$.andEl 3
5.$\EqtMACRoJ {u}{0}$.AddUnits.ext 4
Proof, French
5 lines
1.Soit $u$ un élément de $\mathrm{AddUnits}$ appliqué à $\Natural$.
2.$\EqtMACRoJ {\operatorname{val} (u)+ \operatorname{neg} (u)}{0}$.AddUnits.val_neg
3.$\operatorname{val} (u)= 0$ et $\operatorname{neg} (u)= 0$.Nat.eq_zero_of_add_eq_zero 2
4.$\operatorname{val} (u)= 0$.andEl 3
5.$\EqtMACRoJ {u}{0}$.AddUnits.ext 4
Proof, Czech
5 lines
1.Nechť $u$ je prvek $\mathrm{AddUnits}$ aplikovaný na $\Natural$.
2.$\EqtMACRoJ {\operatorname{val} (u)+ \operatorname{neg} (u)}{0}$.AddUnits.val_neg
3.$\operatorname{val} (u)= 0$ a $\operatorname{neg} (u)= 0$.Nat.eq_zero_of_add_eq_zero 2
4.$\operatorname{val} (u)= 0$.andEl 3
5.$\EqtMACRoJ {u}{0}$.AddUnits.ext 4
Proof, German
5 lines
1.Sei $u$ eine additive Einheit von $\Natural$.
2.AddUnits.val_neg
3.Nat.eq_zero_of_add_eq_zero 2
4.andEl 3
5.$\EqtMACRoJ {u}{0}$.AddUnits.ext 4
Proof, Swedish
5 lines
1.Låt $u$ vara ett element av $\mathrm{AddUnits}$ applicerat på $\Natural$.
2.$\EqtMACRoJ {\operatorname{val} (u)+ \operatorname{neg} (u)}{0}$.AddUnits.val_neg
3.$\operatorname{val} (u)= 0$ och $\operatorname{neg} (u)= 0$.Nat.eq_zero_of_add_eq_zero 2
4.$\operatorname{val} (u)= 0$.andEl 3
5.$\EqtMACRoJ {u}{0}$.AddUnits.ext 4
Nat.isUnit_ifftheoremUnits.lean:38
Alias of isUnit_iff_eq_one for discoverability.
Lean
protected lemma isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 := isUnit_iff_eq_one
Dedukti
2 lines
def Nat__isUnit_iff : (n : Elem Nat) -> Proof (iff (IsUnit n) (Eq n 1)) :=
  n => isUnit_iff_eq_one Nat n.
English
Let $n$ be a natural number. Then $n$ is a unit, if and only if $n = 1$.
French
Soit $n$ un nombre naturel. Alors $n$ est une unité si et seulement si $n = 1$.
Czech
Nechť $n$ je přirozené číslo. Tedy $n$ je jednotka, právě tehdy, když $n = 1$.
German
Sei $n$ eine natürliche Zahl. Dann ist $n$ eine Einheit, genau dann, wenn $n = 1$.
Swedish
Låt $n$ vara ett naturligt tal. Då är $n$ en enhet, om och endast om $n = 1$.
Formula
$n \in \Natural \vdash \mathrm{IsUnit} (n)\leftrightarrow n = 1$
Proof
2 lines
1.Let $n$ be an element of $\Natural$.
2.$n$ is a unit, if and only if $\EqtMACRoJ {n}{1}$.isUnit_iff_eq_one
Proof, French
2 lines
1.Soit $n$ un élément de $\Natural$.
2.$n$ est une unité si et seulement si $\EqtMACRoJ {n}{1}$.isUnit_iff_eq_one
Proof, Czech
2 lines
1.Nechť $n$ je prvek $\Natural$.
2.$n$ je jednotka, právě tehdy, když $\EqtMACRoJ {n}{1}$.isUnit_iff_eq_one
Proof, German
2 lines
1.Sei $n$ ein Element von $\Natural$.
2.$n$ ist eine Einheit, genau dann, wenn $\EqtMACRoJ {n}{1}$.isUnit_iff_eq_one
Proof, Swedish
2 lines
1.Låt $n$ vara ett element av $\Natural$.
2.$n$ är en enhet, om och endast om $\EqtMACRoJ {n}{1}$.isUnit_iff_eq_one
Nat.isAddUnit_ifftheoremUnits.lean:41
Alias of isAddUnit_iff_eq_zero for discoverability.
Lean
protected lemma isAddUnit_iff {n : ℕ} : IsAddUnit n ↔ n = 0 := isAddUnit_iff_eq_zero
Dedukti
2 lines
def Nat__isAddUnit_iff : (n : Elem Nat) -> Proof (iff (IsAddUnit n) (Eq n 0)) :=
  n => isAddUnit_iff_eq_zero Nat n.
English
Let $n$ be a natural number. Then $n$ is an additive unit, if and only if $n = 0$.
French
Soit $n$ un nombre naturel. Alors $n$ est une unité additive si et seulement si $n = 0$.
Czech
Nechť $n$ je přirozené číslo. Tedy $n$ je aditivní jednotka, právě tehdy, když $n = 0$.
German
Sei $n$ eine natürliche Zahl. Dann ist $n$ eine additive Einheit, genau dann, wenn $n = 0$.
Swedish
Låt $n$ vara ett naturligt tal. Då är $n$ en additiv enhet, om och endast om $n = 0$.
Formula
$n \in \Natural \vdash \mathrm{IsAddUnit} (n)\leftrightarrow n = 0$
Proof
2 lines
1.Let $n$ be an element of $\Natural$.
2.$n$ is an additive unit, if and only if $\EqtMACRoJ {n}{0}$.isAddUnit_iff_eq_zero
Proof, French
2 lines
1.Soit $n$ un élément de $\Natural$.
2.$n$ est une unité additive si et seulement si $\EqtMACRoJ {n}{0}$.isAddUnit_iff_eq_zero
Proof, Czech
2 lines
1.Nechť $n$ je prvek $\Natural$.
2.$n$ je aditivní jednotka, právě tehdy, když $\EqtMACRoJ {n}{0}$.isAddUnit_iff_eq_zero
Proof, German
2 lines
1.Sei $n$ ein Element von $\Natural$.
2.$n$ ist eine additive Einheit, genau dann, wenn $\EqtMACRoJ {n}{0}$.isAddUnit_iff_eq_zero
Proof, Swedish
2 lines
1.Låt $n$ vara ett element av $\Natural$.
2.$n$ är en additiv enhet, om och endast om $\EqtMACRoJ {n}{0}$.isAddUnit_iff_eq_zero

Mathlib.Algebra.Prime.Defs source

PrimedefDefs.lean:43
An element p of a commutative monoid with zero (e.g., a ring) is called prime, if it's not zero, not a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b.
Lean
def Prime (p : M) : Prop :=
  p ≠ 0 ∧ ¬IsUnit p ∧ ∀ a b, p ∣ a * b → p ∣ a ∨ p ∣ b
Dedukti
2 lines
def Prime : (p : Elem M) -> Prop :=
  p => and (Neq p 0) (and (not (IsUnit p)) (forall M (a => forall M (b => if (divide p (times a b)) (or (divide p a) (divide p b)))))).
English
Let $p$ be an element of $M$. Then $p$ is prime, if $p \neq 0$, $p$ is not a unit and for all elements $a$ of $M$, for all elements $b$ of $M$, if $p$ divides $a \times b$, then $p$ divides $a$ or $p$ divides $b$.
French
Soit $p$ un élément de $M$. Alors $p$ est premier si $p \neq 0$, $p$ n'est pas une unité et pour tous des éléments $a$ de $M$, pour tous des éléments $b$ de $M$, si $p$ divise $a \times b$, alors $p$ divise $a$ ou $p$ divise $b$.
Czech
Nechť $p$ je prvek $M$. Tedy $p$ je prvočíselné, jestliže $p \neq 0$, $p$ není jednotka a pro všechny prvky $a$ $M$, pro všechny prvky $b$ $M$, jestliže $p$ dělí $a \times b$, pak $p$ dělí $a$ nebo $p$ dělí $b$.
German
Sei $p$ ein Element von $M$. Dann ist $p$ prim, wenn $p \neq 0$, $p$ nicht eine Einheit ist und für alle Elemente $a$ von $M$, für alle Elemente $b$ von $M$, wenn $p$ $a \times b$ teilt, dann $p$ $a$ teilt oder $p$ $b$ teilt.
Swedish
Låt $p$ vara ett element av $M$. Då är $p$ primt, om $p \neq 0$, $p$ inte är en enhet och för alla element $a$ av $M$, för alla element $b$ av $M$, om $p$ delar $a \times b$, så delar $p$ $a$ eller $p$ delar $b$.
Formula
$p \in M \vdash \mathrm{Prime} (p):\Leftrightarrow p \neq 0 \wedge (\neg \mathrm{IsUnit} (p)\wedge (\forall a \in M . \forall b \in M . \divides {p}{a \times b}\rightarrow \divides {p}{a}\vee \divides {p}{b}))$
Prime.ne_zerotheoremDefs.lean:51
Lean
theorem ne_zero : p ≠ 0 :=
  hp.1
Dedukti
2 lines
def Prime__ne_zero : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (Neq p 0) :=
  M => x => p => hp => andEl (Neq p 0) (and (not (IsUnit p)) (forall M (a => forall M (b => if (divide p (times a b)) (or (divide p a) (divide p b)))))) hp.
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ be a prime element of $M$. Then $p \neq 0$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $p$ un élément de $M$ premier. Alors $p \neq 0$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ je prvočíselný prvek $M$. Tedy $p \neq 0$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $p$ ein primes Element von $M$. Dann $p \neq 0$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ vara ett primt element av $M$. Då $p \neq 0$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p)\vdash p \neq 0$
Proof
3 lines
1.Let $p$ be an element of $M$.
2.Assume that $p$ is prime.
3.$p \neq 0$.andEl 2
Proof, French
3 lines
1.Soit $p$ un élément de $M$.
2.Supposons que $p$ est premier.
3.$p \neq 0$.andEl 2
Proof, Czech
3 lines
1.Nechť $p$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.$p \neq 0$.andEl 2
Proof, German
3 lines
1.Sei $p$ ein Element von $M$.
2.Nimm an, dass $p$ prim ist.
3.$p \neq 0$.andEl 2
Proof, Swedish
3 lines
1.Låt $p$ vara ett element av $M$.
2.Anta att $p$ är primt.
3.$p \neq 0$.andEl 2
Prime.not_isUnittheoremDefs.lean:54
Lean
theorem not_isUnit : ¬IsUnit p :=
  hp.2.1
Dedukti
2 lines
def Prime__not_isUnit : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (not (IsUnit p)) :=
  M => x => p => hp => andEl (not (IsUnit p)) (forall M (a => forall M (b => if (divide p (times a b)) (or (divide p a) (divide p b))))) (andEr (Neq p 0) (and (not (IsUnit p)) (forall M (a1 => forall M (b1 => if (divide p (times a1 b1)) (or (divide p a1) (divide p b1)))))) hp).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ be a prime element of $M$. Then $p$ is not a unit.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $p$ un élément de $M$ premier. Alors $p$ n'est pas une unité.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ je prvočíselný prvek $M$. Tedy $p$ není jednotka.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $p$ ein primes Element von $M$. Dann ist $p$ nicht eine Einheit.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ vara ett primt element av $M$. Då är $p$ inte en enhet.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p)\vdash \neg \mathrm{IsUnit} (p)$
Proof
4 lines
1.Let $p$ be an element of $M$.
2.Assume that $p$ is prime.
3.$p$ is not a unit and for all elements $a_{1}$ of $M$, for all elements $b_{1}$ of $M$, if $\divides {p}{a_{1} \times b_{1}}$, then $\divides {p}{a_{1}}$ or $\divides {p}{b_{1}}$.andEr 2
4.$p$ is not a unit.andEl 3
Proof, French
4 lines
1.Soit $p$ un élément de $M$.
2.Supposons que $p$ est premier.
3.$p$ n'est pas une unité et pour tous des éléments $a_{1}$ de $M$, pour tous des éléments $b_{1}$ de $M$, si $\divides {p}{a_{1} \times b_{1}}$, alors $\divides {p}{a_{1}}$ ou $\divides {p}{b_{1}}$.andEr 2
4.$p$ n'est pas une unité.andEl 3
Proof, Czech
4 lines
1.Nechť $p$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.$p$ není jednotka a pro všechny prvky $a_{1}$ $M$, pro všechny prvky $b_{1}$ $M$, jestliže $\divides {p}{a_{1} \times b_{1}}$, pak $\divides {p}{a_{1}}$ nebo $\divides {p}{b_{1}}$.andEr 2
4.$p$ není jednotka.andEl 3
Proof, German
4 lines
1.Sei $p$ ein Element von $M$.
2.Nimm an, dass $p$ prim ist.
3.$p$ ist nicht eine Einheit und für alle Elemente $a_{1}$ von $M$, für alle Elemente $b_{1}$ von $M$, wenn $\divides {p}{a_{1} \times b_{1}}$, dann $\divides {p}{a_{1}}$ oder $\divides {p}{b_{1}}$.andEr 2
4.$p$ ist nicht eine Einheit.andEl 3
Proof, Swedish
4 lines
1.Låt $p$ vara ett element av $M$.
2.Anta att $p$ är primt.
3.$p$ är inte en enhet och för alla element $a_{1}$ av $M$, för alla element $b_{1}$ av $M$, om $\divides {p}{a_{1} \times b_{1}}$, så $\divides {p}{a_{1}}$ eller $\divides {p}{b_{1}}$.andEr 2
4.$p$ är inte en enhet.andEl 3
Prime.not_dvd_onetheoremDefs.lean:60
Lean
theorem not_dvd_one : ¬p ∣ 1 :=
  mt (isUnit_of_dvd_one ·) hp.not_isUnit
Dedukti
2 lines
def Prime__not_dvd_one : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (not (divide p 1)) :=
  M => x => p => hp => mt (divide p 1) (IsUnit p) (ifI (divide p 1) (IsUnit p) (h => isUnit_of_dvd_one M p h)) (Prime__not_isUnit M p hp).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ be a prime element of $M$. Then $p$ does not divide $1$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $p$ un élément de $M$ premier. Alors $p$ ne divise pas $1$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ je prvočíselný prvek $M$. Tedy $p$ nedělí $1$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $p$ ein primes Element von $M$. Dann teilt $p$ nicht $1$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ vara ett primt element av $M$. Då delar $p$ inte $1$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p)\vdash \neg (\divides {p}{1})$
Proof
7 lines
1.Let $p$ be an element of $M$.
2.Assume that $\divides {p}{1}$.
3.$p$ is a unit.isUnit_of_dvd_one 2
4.If $\divides {p}{1}$, then $p$ is a unit.ifI 3 [h]
5.Assume that $p$ is prime.
6.$p$ is not a unit.Prime.not_isUnit 5
7.It is not the case that $\divides {p}{1}$.mt 4, 6
Proof, French
7 lines
1.Soit $p$ un élément de $M$.
2.Supposons que $\divides {p}{1}$.
3.$p$ est une unité.isUnit_of_dvd_one 2
4.Si $\divides {p}{1}$, alors $p$ est une unité.ifI 3 [h]
5.Supposons que $p$ est premier.
6.$p$ n'est pas une unité.Prime.not_isUnit 5
7.Il n'est pas le cas que $\divides {p}{1}$.mt 4, 6
Proof, Czech
7 lines
1.Nechť $p$ je prvek $M$.
2.Předpokládejme, že $\divides {p}{1}$.
3.$p$ je jednotka.isUnit_of_dvd_one 2
4.Jestliže $\divides {p}{1}$, pak $p$ je jednotka.ifI 3 [h]
5.Předpokládejme, že $p$ je prvočíselné.
6.$p$ není jednotka.Prime.not_isUnit 5
7.Není případ že $\divides {p}{1}$.mt 4, 6
Proof, German
7 lines
1.Sei $p$ ein Element von $M$.
2.Nimm an, dass $\divides {p}{1}$.
3.$p$ ist eine Einheit.isUnit_of_dvd_one 2
4.Wenn $\divides {p}{1}$, dann ist $p$ eine Einheit.ifI 3 [h]
5.Nimm an, dass $p$ prim ist.
6.$p$ ist nicht eine Einheit.Prime.not_isUnit 5
7.Es ist nicht der Fall dass $\divides {p}{1}$.mt 4, 6
Proof, Swedish
7 lines
1.Låt $p$ vara ett element av $M$.
2.Anta att $\divides {p}{1}$.
3.$p$ är en enhet.isUnit_of_dvd_one 2
4.Om $\divides {p}{1}$, så är $p$ en enhet.ifI 3 [h]
5.Anta att $p$ är primt.
6.$p$ är inte en enhet.Prime.not_isUnit 5
7.Det är inte fallet att $\divides {p}{1}$.mt 4, 6
Prime.ne_onetheoremDefs.lean:63
Lean
theorem ne_one : p ≠ 1 :=
Dedukti
1 lines
Prime__ne_one : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (Neq p 1).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ be a prime element of $M$. Then $p \neq 1$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $p$ un élément de $M$ premier. Alors $p \neq 1$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ je prvočíselný prvek $M$. Tedy $p \neq 1$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $p$ ein primes Element von $M$. Dann $p \neq 1$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ vara ett primt element av $M$. Då $p \neq 1$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p)\vdash p \neq 1$
Prime.dvd_or_dvdtheoremDefs.lean:65
Lean
theorem dvd_or_dvd {a b : M} (h : p ∣ a * b) : p ∣ a ∨ p ∣ b :=
  hp.2.2 a b h
Dedukti
2 lines
def Prime__dvd_or_dvd : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> (a : Elem M) -> (b : Elem M) -> (h : Proof (divide p (times a b))) -> Proof (or (divide p a) (divide p b)) :=
  M => x => p => hp => a => b => h => andEr (not (IsUnit p)) (forall M (a1 => forall M (b1 => if (divide p (times a1 b1)) (or (divide p a1) (divide p b1))))) (andEr (Neq p 0) (and (not (IsUnit p)) (forall M (a2 => forall M (b2 => if (divide p (times a2 b2)) (or (divide p a2) (divide p b2)))))) hp) a b h.
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$, $a$ and $b$ be elements of $M$ such that $p$ is prime and $p$ divides $a \times b$. Then $p$ divides $a$ or $p$ divides $b$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soient $p$, $a$ et $b$ des éléments de $M$ tels que $p$ soit premier et $p$ divise $a \times b$. Alors $p$ divise $a$ ou $p$ divise $b$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$, $a$ a $b$ je prvek $M$ takový, že $p$ je prvočíselné a $p$ dělí $a \times b$. Tedy $p$ dělí $a$ nebo $p$ dělí $b$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Seien $p$, $a$ und $b$ elemente von $M$ derart, dass $p$ prim ist und $p$ $a \times b$ teilt. Dann teilt $p$ $a$ oder $p$ teilt $b$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$, $a$ och $b$ vara element av $M$ sådana att $p$ är primt och $p$ delar $a \times b$. Då delar $p$ $a$ eller $p$ delar $b$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p), a , b \in M , \divides {p}{a \times b}\vdash \divides {p}{a}\vee \divides {p}{b}$
Proof
4 lines
1.Let $p$, $a$ and $b$ be elements of $M$.
2.Assume that $p$ is prime.
3.$p$ is not a unit and for all elements $a_{2}$ of $M$, for all elements $b_{2}$ of $M$, if $\divides {p}{a_{2} \times b_{2}}$, then $\divides {p}{a_{2}}$ or $\divides {p}{b_{2}}$.andEr 2
4.For all elements $a_{1}$ and $b_{1}$ of $M$, if $\divides {p}{a_{1} \times b_{1}}$, then $\divides {p}{a_{1}}$ or $\divides {p}{b_{1}}$.andEr 3
Proof, French
4 lines
1.Soient $p$, $a$ et $b$ des éléments de $M$.
2.Supposons que $p$ est premier.
3.$p$ n'est pas une unité et pour tous des éléments $a_{2}$ de $M$, pour tous des éléments $b_{2}$ de $M$, si $\divides {p}{a_{2} \times b_{2}}$, alors $\divides {p}{a_{2}}$ ou $\divides {p}{b_{2}}$.andEr 2
4.Pour tous les éléments $a_{1}$ et $b_{1}$ de $M$, si $\divides {p}{a_{1} \times b_{1}}$, alors $\divides {p}{a_{1}}$ ou $\divides {p}{b_{1}}$.andEr 3
Proof, Czech
4 lines
1.Nechť $p$, $a$ a $b$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.$p$ není jednotka a pro všechny prvky $a_{2}$ $M$, pro všechny prvky $b_{2}$ $M$, jestliže $\divides {p}{a_{2} \times b_{2}}$, pak $\divides {p}{a_{2}}$ nebo $\divides {p}{b_{2}}$.andEr 2
4.Pro všechny prvky $a_{1}$ a $b_{1}$ $M$, jestliže $\divides {p}{a_{1} \times b_{1}}$, pak $\divides {p}{a_{1}}$ nebo $\divides {p}{b_{1}}$.andEr 3
Proof, German
4 lines
1.Seien $p$, $a$ und $b$ elemente von $M$.
2.Nimm an, dass $p$ prim ist.
3.$p$ ist nicht eine Einheit und für alle Elemente $a_{2}$ von $M$, für alle Elemente $b_{2}$ von $M$, wenn $\divides {p}{a_{2} \times b_{2}}$, dann $\divides {p}{a_{2}}$ oder $\divides {p}{b_{2}}$.andEr 2
4.Für alle Elemente $a_{1}$ und $b_{1}$ von $M$, wenn $\divides {p}{a_{1} \times b_{1}}$, dann $\divides {p}{a_{1}}$ oder $\divides {p}{b_{1}}$.andEr 3
Proof, Swedish
4 lines
1.Låt $p$, $a$ och $b$ vara element av $M$.
2.Anta att $p$ är primt.
3.$p$ är inte en enhet och för alla element $a_{2}$ av $M$, för alla element $b_{2}$ av $M$, om $\divides {p}{a_{2} \times b_{2}}$, så $\divides {p}{a_{2}}$ eller $\divides {p}{b_{2}}$.andEr 2
4.För alla element $a_{1}$ och $b_{1}$ av $M$, om $\divides {p}{a_{1} \times b_{1}}$, så $\divides {p}{a_{1}}$ eller $\divides {p}{b_{1}}$.andEr 3
Prime.dvd_multheoremDefs.lean:68
Lean
theorem dvd_mul {a b : M} : p ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
  ⟨hp.dvd_or_dvd, (Or.elim · (dvd_mul_of_dvd_left · _) (dvd_mul_of_dvd_right · _))⟩
Dedukti
2 lines
def Prime__dvd_mul : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> (a : Elem M) -> (b : Elem M) -> Proof (iff (divide p (times a b)) (or (divide p a) (divide p b))) :=
  M => x => p => hp => a => b => iffI (divide p (times a b)) (or (divide p a) (divide p b)) (Prime__dvd_or_dvd M p hp a b) (h => orE (divide p a) (divide p b) (divide p (times a b)) h (h1 => dvd_mul_of_dvd_left M p a h1 b) (h2 => dvd_mul_of_dvd_right M p b h2 a)).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$, $a$ and $b$ be elements of $M$ such that $p$ is prime. Then $p$ divides $a \times b$, if and only if $p$ divides $a$ or $p$ divides $b$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soient $p$, $a$ et $b$ des éléments de $M$ tels que $p$ soit premier. Alors $p$ divise $a \times b$ si et seulement si $p$ divise $a$ ou $p$ divise $b$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$, $a$ a $b$ je prvek $M$ takový, že $p$ je prvočíselné. Tedy $p$ dělí $a \times b$, právě tehdy, když $p$ dělí $a$ nebo $p$ dělí $b$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Seien $p$, $a$ und $b$ elemente von $M$ derart, dass $p$ prim ist. Dann teilt $p$ $a \times b$, genau dann, wenn $p$ $a$ teilt oder $p$ $b$ teilt.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$, $a$ och $b$ vara element av $M$ sådana att $p$ är primt. Då delar $p$ $a \times b$, om och endast om $p$ delar $a$ eller $p$ delar $b$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p), a , b \in M \vdash \divides {p}{a \times b}\leftrightarrow \divides {p}{a}\vee \divides {p}{b}$
Proof
10 lines
1.Let $p$, $a$ and $b$ be elements of $M$.
2.Assume that $p$ is prime.
3.$\divides {p}{a}$ or $\divides {p}{b}$.Prime.dvd_or_dvd 2
4.Assume that $\divides {p}{a}$ or $\divides {p}{b}$.
5.Assume that $\divides {p}{a}$.
6.$\divides {p}{a \times b}$.dvd_mul_of_dvd_left 5
7.Assume that $\divides {p}{b}$.
8.$\divides {p}{a \times b}$.dvd_mul_of_dvd_right 7
9.$\divides {p}{a \times b}$.orE 4, 6, 8 [h1, h2]
10.$\divides {p}{a \times b}$, if and only if $\divides {p}{a}$ or $\divides {p}{b}$.iffI 3, 9 [h]
Proof, French
10 lines
1.Soient $p$, $a$ et $b$ des éléments de $M$.
2.Supposons que $p$ est premier.
3.$\divides {p}{a}$ ou $\divides {p}{b}$.Prime.dvd_or_dvd 2
4.Supposons que $\divides {p}{a}$ ou $\divides {p}{b}$.
5.Supposons que $\divides {p}{a}$.
6.$\divides {p}{a \times b}$.dvd_mul_of_dvd_left 5
7.Supposons que $\divides {p}{b}$.
8.$\divides {p}{a \times b}$.dvd_mul_of_dvd_right 7
9.$\divides {p}{a \times b}$.orE 4, 6, 8 [h1, h2]
10.$\divides {p}{a \times b}$ si et seulement si $\divides {p}{a}$ ou $\divides {p}{b}$.iffI 3, 9 [h]
Proof, Czech
10 lines
1.Nechť $p$, $a$ a $b$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.$\divides {p}{a}$ nebo $\divides {p}{b}$.Prime.dvd_or_dvd 2
4.Předpokládejme, že $\divides {p}{a}$ nebo $\divides {p}{b}$.
5.Předpokládejme, že $\divides {p}{a}$.
6.$\divides {p}{a \times b}$.dvd_mul_of_dvd_left 5
7.Předpokládejme, že $\divides {p}{b}$.
8.$\divides {p}{a \times b}$.dvd_mul_of_dvd_right 7
9.$\divides {p}{a \times b}$.orE 4, 6, 8 [h1, h2]
10.$\divides {p}{a \times b}$, právě tehdy, když $\divides {p}{a}$ nebo $\divides {p}{b}$.iffI 3, 9 [h]
Proof, German
10 lines
1.Seien $p$, $a$ und $b$ elemente von $M$.
2.Nimm an, dass $p$ prim ist.
3.$\divides {p}{a}$ oder $\divides {p}{b}$.Prime.dvd_or_dvd 2
4.Nimm an, dass $\divides {p}{a}$ oder $\divides {p}{b}$.
5.Nimm an, dass $\divides {p}{a}$.
6.$\divides {p}{a \times b}$.dvd_mul_of_dvd_left 5
7.Nimm an, dass $\divides {p}{b}$.
8.$\divides {p}{a \times b}$.dvd_mul_of_dvd_right 7
9.$\divides {p}{a \times b}$.orE 4, 6, 8 [h1, h2]
10.$\divides {p}{a \times b}$, genau dann, wenn $\divides {p}{a}$ oder $\divides {p}{b}$.iffI 3, 9 [h]
Proof, Swedish
10 lines
1.Låt $p$, $a$ och $b$ vara element av $M$.
2.Anta att $p$ är primt.
3.$\divides {p}{a}$ eller $\divides {p}{b}$.Prime.dvd_or_dvd 2
4.Anta att $\divides {p}{a}$ eller $\divides {p}{b}$.
5.Anta att $\divides {p}{a}$.
6.$\divides {p}{a \times b}$.dvd_mul_of_dvd_left 5
7.Anta att $\divides {p}{b}$.
8.$\divides {p}{a \times b}$.dvd_mul_of_dvd_right 7
9.$\divides {p}{a \times b}$.orE 4, 6, 8 [h1, h2]
10.$\divides {p}{a \times b}$, om och endast om $\divides {p}{a}$ eller $\divides {p}{b}$.iffI 3, 9 [h]
Prime.isPrimaltheoremDefs.lean:71
Lean
theorem isPrimal : IsPrimal p := fun _a _b dvd ↦ (hp.dvd_or_dvd dvd).elim
  (fun h ↦ ⟨p, 1, h, one_dvd _, (mul_one p).symm⟩) fun h ↦ ⟨1, p, one_dvd _, h, (one_mul p).symm⟩
Dedukti
2 lines
def Prime__isPrimal : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (IsPrimal p) :=
  M => x => p => hp => forallI M (_a => forall M (_b1 => if (divide p (times _a _b1)) (exists M (x13 => exists M (x14 => and (divide x13 _a) (and (divide x14 _b1) (Eqt M p (times x13 x14)))))))) (_a => forallI M (_b => if (divide p (times _a _b)) (exists M (x11 => exists M (x12 => and (divide x11 _a) (and (divide x12 _b) (Eqt M p (times x11 x12))))))) (_b => ifI (divide p (times _a _b)) (exists M (x9 => exists M (x10 => and (divide x9 _a) (and (divide x10 _b) (Eqt M p (times x9 x10)))))) (dvd => orE (divide p _a) (divide p _b) (exists M (x1 => exists M (x2 => and (divide x1 _a) (and (divide x2 _b) (Eqt M p (times x1 x2)))))) (Prime__dvd_or_dvd M p hp _a _b dvd) (h => existsI M (x3 => exists M (x4 => and (divide x3 _a) (and (divide x4 _b) (Eqt M p (times x3 x4))))) p (existsI M (x5 => and (divide p _a) (and (divide x5 _b) (Eqt M p (times p x5)))) 1 (andI (divide p _a) (and (divide 1 _b) (Eqt M p (times p 1))) h (andI (divide 1 _b) (Eqt M p (times p 1)) (one_dvd M _b) (Eq__symm M (times p 1) p (mul_one M p)))))) (h1 => existsI M (x6 => exists M (x7 => and (divide x6 _a) (and (divide x7 _b) (Eqt M p (times x6 x7))))) 1 (existsI M (x8 => and (divide 1 _a) (and (divide x8 _b) (Eqt M p (times 1 x8)))) p (andI (divide 1 _a) (and (divide p _b) (Eqt M p (times 1 p))) (one_dvd M _a) (andI (divide p _b) (Eqt M p (times 1 p)) h1 (Eq__symm M (times 1 p) p (one_mul M p))))))))).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ be a prime element of $M$. Then $p$ is primal.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $p$ un élément de $M$ premier. Alors $p$ est primal.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ je prvočíselný prvek $M$. Tedy $p$ je prvotní.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $p$ ein primes Element von $M$. Dann ist $p$ primal.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ vara ett primt element av $M$. Då är $p$ primalt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p)\vdash \mathrm{IsPrimal} (p)$
Proof
24 lines
1.Let $p$, $\mathrm{\_a}$ and $\mathrm{\_b}$ be elements of $M$.
2.Assume that $p$ is prime.
3.Assume that $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$.
4.$\divides {p}{\mathrm{\_a}}$ or $\divides {p}{\mathrm{\_b}}$.Prime.dvd_or_dvd 2, 3
5.Assume that $\divides {p}{\mathrm{\_a}}$.
6.$\divides {1}{\mathrm{\_b}}$.one_dvd
7.$\EqtMACRoJ {p \times 1}{p}$.mul_one
8.$\EqtMACRoJ {p}{p \times 1}$.Eq.symm 7
9.$\divides {1}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{p \times 1}$.andI 6, 8
10.$\divides {p}{\mathrm{\_a}}$, $\divides {1}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{p \times 1}$.andI 5, 9
11.There exists an element $x_{5}$ of $M$, such that $\divides {p}{\mathrm{\_a}}$, $\divides {x_{5}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{p \times x_{5}}$.existsI 10
12.There exist elements $x_{3}$ and $x_{4}$ of $M$, such that $\divides {x_{3}}{\mathrm{\_a}}$, $\divides {x_{4}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{x_{3} \times x_{4}}$.existsI 11
13.$\divides {1}{\mathrm{\_a}}$.one_dvd
14.Assume that $\divides {p}{\mathrm{\_b}}$.
15.$\EqtMACRoJ {1 \times p}{p}$.one_mul
16.$\EqtMACRoJ {p}{1 \times p}$.Eq.symm 15
17.$\divides {p}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{1 \times p}$.andI 14, 16
18.$\divides {1}{\mathrm{\_a}}$, $\divides {p}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{1 \times p}$.andI 13, 17
19.There exists an element $x_{8}$ of $M$, such that $\divides {1}{\mathrm{\_a}}$, $\divides {x_{8}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{1 \times x_{8}}$.existsI 18
20.There exist elements $x_{6}$ and $x_{7}$ of $M$, such that $\divides {x_{6}}{\mathrm{\_a}}$, $\divides {x_{7}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{x_{6} \times x_{7}}$.existsI 19
21.There exist elements $x_{1}$ and $x_{2}$ of $M$, such that $\divides {x_{1}}{\mathrm{\_a}}$, $\divides {x_{2}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{x_{1} \times x_{2}}$.orE 4, 12, 20 [h, h1]
22.If $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, then there exist elements $x_{9}$ and $x_{10}$ of $M$, such that $\divides {x_{9}}{\mathrm{\_a}}$, $\divides {x_{10}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{x_{9} \times x_{10}}$.ifI 21 [dvd]
23.For all elements $\mathrm{\_b}$ of $M$, if $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, then there exist elements $x_{11}$ and $x_{12}$ of $M$, such that $\divides {x_{11}}{\mathrm{\_a}}$, $\divides {x_{12}}{\mathrm{\_b}}$ and $\EqtMACRoJ {p}{x_{11} \times x_{12}}$.forallI 1, 22 [_b]
24.For all elements $\mathrm{\_a}$ and $\mathrm{\_b1}$ of $M$, if $\divides {p}{\mathrm{\_a} \times \mathrm{\_b1}}$, then there exist elements $x_{13}$ and $x_{14}$ of $M$, such that $\divides {x_{13}}{\mathrm{\_a}}$, $\divides {x_{14}}{\mathrm{\_b1}}$ and $\EqtMACRoJ {p}{x_{13} \times x_{14}}$.forallI 1, 23 [_a]
Proof, French
24 lines
1.Soient $p$, $\mathrm{\_a}$ et $\mathrm{\_b}$ des éléments de $M$.
2.Supposons que $p$ est premier.
3.Supposons que $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$.
4.$\divides {p}{\mathrm{\_a}}$ ou $\divides {p}{\mathrm{\_b}}$.Prime.dvd_or_dvd 2, 3
5.Supposons que $\divides {p}{\mathrm{\_a}}$.
6.$\divides {1}{\mathrm{\_b}}$.one_dvd
7.$\EqtMACRoJ {p \times 1}{p}$.mul_one
8.$\EqtMACRoJ {p}{p \times 1}$.Eq.symm 7
9.$\divides {1}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{p \times 1}$.andI 6, 8
10.$\divides {p}{\mathrm{\_a}}$, $\divides {1}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{p \times 1}$.andI 5, 9
11.Il existe un élément $x_{5}$ de $M$ tel que $\divides {p}{\mathrm{\_a}}$, $\divides {x_{5}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{p \times x_{5}}$.existsI 10
12.Il existent des éléments $x_{3}$ et $x_{4}$ de $M$ tel que $\divides {x_{3}}{\mathrm{\_a}}$, $\divides {x_{4}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{x_{3} \times x_{4}}$.existsI 11
13.$\divides {1}{\mathrm{\_a}}$.one_dvd
14.Supposons que $\divides {p}{\mathrm{\_b}}$.
15.$\EqtMACRoJ {1 \times p}{p}$.one_mul
16.$\EqtMACRoJ {p}{1 \times p}$.Eq.symm 15
17.$\divides {p}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{1 \times p}$.andI 14, 16
18.$\divides {1}{\mathrm{\_a}}$, $\divides {p}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{1 \times p}$.andI 13, 17
19.Il existe un élément $x_{8}$ de $M$ tel que $\divides {1}{\mathrm{\_a}}$, $\divides {x_{8}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{1 \times x_{8}}$.existsI 18
20.Il existent des éléments $x_{6}$ et $x_{7}$ de $M$ tel que $\divides {x_{6}}{\mathrm{\_a}}$, $\divides {x_{7}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{x_{6} \times x_{7}}$.existsI 19
21.Il existent des éléments $x_{1}$ et $x_{2}$ de $M$ tel que $\divides {x_{1}}{\mathrm{\_a}}$, $\divides {x_{2}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{x_{1} \times x_{2}}$.orE 4, 12, 20 [h, h1]
22.Si $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, alors il existent des éléments $x_{9}$ et $x_{10}$ de $M$ tel que $\divides {x_{9}}{\mathrm{\_a}}$, $\divides {x_{10}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{x_{9} \times x_{10}}$.ifI 21 [dvd]
23.Pour tous les éléments $\mathrm{\_b}$ de $M$, si $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, alors il existent des éléments $x_{11}$ et $x_{12}$ de $M$ tel que $\divides {x_{11}}{\mathrm{\_a}}$, $\divides {x_{12}}{\mathrm{\_b}}$ et $\EqtMACRoJ {p}{x_{11} \times x_{12}}$.forallI 1, 22 [_b]
24.Pour tous les éléments $\mathrm{\_a}$ et $\mathrm{\_b1}$ de $M$, si $\divides {p}{\mathrm{\_a} \times \mathrm{\_b1}}$, alors il existent des éléments $x_{13}$ et $x_{14}$ de $M$ tel que $\divides {x_{13}}{\mathrm{\_a}}$, $\divides {x_{14}}{\mathrm{\_b1}}$ et $\EqtMACRoJ {p}{x_{13} \times x_{14}}$.forallI 1, 23 [_a]
Proof, Czech
24 lines
1.Nechť $p$, $\mathrm{\_a}$ a $\mathrm{\_b}$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.Předpokládejme, že $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$.
4.$\divides {p}{\mathrm{\_a}}$ nebo $\divides {p}{\mathrm{\_b}}$.Prime.dvd_or_dvd 2, 3
5.Předpokládejme, že $\divides {p}{\mathrm{\_a}}$.
6.$\divides {1}{\mathrm{\_b}}$.one_dvd
7.$\EqtMACRoJ {p \times 1}{p}$.mul_one
8.$\EqtMACRoJ {p}{p \times 1}$.Eq.symm 7
9.$\divides {1}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{p \times 1}$.andI 6, 8
10.$\divides {p}{\mathrm{\_a}}$, $\divides {1}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{p \times 1}$.andI 5, 9
11.Existuje prvek $x_{5}$ $M$, takový, že $\divides {p}{\mathrm{\_a}}$, $\divides {x_{5}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{p \times x_{5}}$.existsI 10
12.Existují prvky $x_{3}$ a $x_{4}$ $M$, takový, že $\divides {x_{3}}{\mathrm{\_a}}$, $\divides {x_{4}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{x_{3} \times x_{4}}$.existsI 11
13.$\divides {1}{\mathrm{\_a}}$.one_dvd
14.Předpokládejme, že $\divides {p}{\mathrm{\_b}}$.
15.$\EqtMACRoJ {1 \times p}{p}$.one_mul
16.$\EqtMACRoJ {p}{1 \times p}$.Eq.symm 15
17.$\divides {p}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{1 \times p}$.andI 14, 16
18.$\divides {1}{\mathrm{\_a}}$, $\divides {p}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{1 \times p}$.andI 13, 17
19.Existuje prvek $x_{8}$ $M$, takový, že $\divides {1}{\mathrm{\_a}}$, $\divides {x_{8}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{1 \times x_{8}}$.existsI 18
20.Existují prvky $x_{6}$ a $x_{7}$ $M$, takový, že $\divides {x_{6}}{\mathrm{\_a}}$, $\divides {x_{7}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{x_{6} \times x_{7}}$.existsI 19
21.Existují prvky $x_{1}$ a $x_{2}$ $M$, takový, že $\divides {x_{1}}{\mathrm{\_a}}$, $\divides {x_{2}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{x_{1} \times x_{2}}$.orE 4, 12, 20 [h, h1]
22.Jestliže $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, pak existují prvky $x_{9}$ a $x_{10}$ $M$, takový, že $\divides {x_{9}}{\mathrm{\_a}}$, $\divides {x_{10}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{x_{9} \times x_{10}}$.ifI 21 [dvd]
23.Pro všechny prvky $\mathrm{\_b}$ $M$, jestliže $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, pak existují prvky $x_{11}$ a $x_{12}$ $M$, takový, že $\divides {x_{11}}{\mathrm{\_a}}$, $\divides {x_{12}}{\mathrm{\_b}}$ a $\EqtMACRoJ {p}{x_{11} \times x_{12}}$.forallI 1, 22 [_b]
24.Pro všechny prvky $\mathrm{\_a}$ a $\mathrm{\_b1}$ $M$, jestliže $\divides {p}{\mathrm{\_a} \times \mathrm{\_b1}}$, pak existují prvky $x_{13}$ a $x_{14}$ $M$, takový, že $\divides {x_{13}}{\mathrm{\_a}}$, $\divides {x_{14}}{\mathrm{\_b1}}$ a $\EqtMACRoJ {p}{x_{13} \times x_{14}}$.forallI 1, 23 [_a]
Proof, German
24 lines
1.Seien $p$, $\mathrm{\_a}$ und $\mathrm{\_b}$ elemente von $M$.
2.Nimm an, dass $p$ prim ist.
3.Nimm an, dass $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$.
4.$\divides {p}{\mathrm{\_a}}$ oder $\divides {p}{\mathrm{\_b}}$.Prime.dvd_or_dvd 2, 3
5.Nimm an, dass $\divides {p}{\mathrm{\_a}}$.
6.$\divides {1}{\mathrm{\_b}}$.one_dvd
7.$\EqtMACRoJ {p \times 1}{p}$.mul_one
8.$\EqtMACRoJ {p}{p \times 1}$.Eq.symm 7
9.$\divides {1}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{p \times 1}$.andI 6, 8
10.$\divides {p}{\mathrm{\_a}}$, $\divides {1}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{p \times 1}$.andI 5, 9
11.Es gibt ein Element $x_{5}$ von $M$, derart, dass $\divides {p}{\mathrm{\_a}}$, $\divides {x_{5}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{p \times x_{5}}$.existsI 10
12.Es gibt Elemente $x_{3}$ und $x_{4}$ von $M$, derart, dass $\divides {x_{3}}{\mathrm{\_a}}$, $\divides {x_{4}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{x_{3} \times x_{4}}$.existsI 11
13.$\divides {1}{\mathrm{\_a}}$.one_dvd
14.Nimm an, dass $\divides {p}{\mathrm{\_b}}$.
15.$\EqtMACRoJ {1 \times p}{p}$.one_mul
16.$\EqtMACRoJ {p}{1 \times p}$.Eq.symm 15
17.$\divides {p}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{1 \times p}$.andI 14, 16
18.$\divides {1}{\mathrm{\_a}}$, $\divides {p}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{1 \times p}$.andI 13, 17
19.Es gibt ein Element $x_{8}$ von $M$, derart, dass $\divides {1}{\mathrm{\_a}}$, $\divides {x_{8}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{1 \times x_{8}}$.existsI 18
20.Es gibt Elemente $x_{6}$ und $x_{7}$ von $M$, derart, dass $\divides {x_{6}}{\mathrm{\_a}}$, $\divides {x_{7}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{x_{6} \times x_{7}}$.existsI 19
21.Es gibt Elemente $x_{1}$ und $x_{2}$ von $M$, derart, dass $\divides {x_{1}}{\mathrm{\_a}}$, $\divides {x_{2}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{x_{1} \times x_{2}}$.orE 4, 12, 20 [h, h1]
22.Wenn $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, dann gibt es Elemente $x_{9}$ und $x_{10}$ von $M$, derart, dass $\divides {x_{9}}{\mathrm{\_a}}$, $\divides {x_{10}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{x_{9} \times x_{10}}$.ifI 21 [dvd]
23.Für alle Elemente $\mathrm{\_b}$ von $M$, wenn $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, dann gibt es Elemente $x_{11}$ und $x_{12}$ von $M$, derart, dass $\divides {x_{11}}{\mathrm{\_a}}$, $\divides {x_{12}}{\mathrm{\_b}}$ und $\EqtMACRoJ {p}{x_{11} \times x_{12}}$.forallI 1, 22 [_b]
24.Für alle Elemente $\mathrm{\_a}$ und $\mathrm{\_b1}$ von $M$, wenn $\divides {p}{\mathrm{\_a} \times \mathrm{\_b1}}$, dann gibt es Elemente $x_{13}$ und $x_{14}$ von $M$, derart, dass $\divides {x_{13}}{\mathrm{\_a}}$, $\divides {x_{14}}{\mathrm{\_b1}}$ und $\EqtMACRoJ {p}{x_{13} \times x_{14}}$.forallI 1, 23 [_a]
Proof, Swedish
24 lines
1.Låt $p$, $\mathrm{\_a}$ och $\mathrm{\_b}$ vara element av $M$.
2.Anta att $p$ är primt.
3.Anta att $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$.
4.$\divides {p}{\mathrm{\_a}}$ eller $\divides {p}{\mathrm{\_b}}$.Prime.dvd_or_dvd 2, 3
5.Anta att $\divides {p}{\mathrm{\_a}}$.
6.$\divides {1}{\mathrm{\_b}}$.one_dvd
7.$\EqtMACRoJ {p \times 1}{p}$.mul_one
8.$\EqtMACRoJ {p}{p \times 1}$.Eq.symm 7
9.$\divides {1}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{p \times 1}$.andI 6, 8
10.$\divides {p}{\mathrm{\_a}}$, $\divides {1}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{p \times 1}$.andI 5, 9
11.Det finns ett element $x_{5}$ av $M$, så att $\divides {p}{\mathrm{\_a}}$, $\divides {x_{5}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{p \times x_{5}}$.existsI 10
12.Det finns element $x_{3}$ och $x_{4}$ av $M$, så att $\divides {x_{3}}{\mathrm{\_a}}$, $\divides {x_{4}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{x_{3} \times x_{4}}$.existsI 11
13.$\divides {1}{\mathrm{\_a}}$.one_dvd
14.Anta att $\divides {p}{\mathrm{\_b}}$.
15.$\EqtMACRoJ {1 \times p}{p}$.one_mul
16.$\EqtMACRoJ {p}{1 \times p}$.Eq.symm 15
17.$\divides {p}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{1 \times p}$.andI 14, 16
18.$\divides {1}{\mathrm{\_a}}$, $\divides {p}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{1 \times p}$.andI 13, 17
19.Det finns ett element $x_{8}$ av $M$, så att $\divides {1}{\mathrm{\_a}}$, $\divides {x_{8}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{1 \times x_{8}}$.existsI 18
20.Det finns element $x_{6}$ och $x_{7}$ av $M$, så att $\divides {x_{6}}{\mathrm{\_a}}$, $\divides {x_{7}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{x_{6} \times x_{7}}$.existsI 19
21.Det finns element $x_{1}$ och $x_{2}$ av $M$, så att $\divides {x_{1}}{\mathrm{\_a}}$, $\divides {x_{2}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{x_{1} \times x_{2}}$.orE 4, 12, 20 [h, h1]
22.Om $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, så finns det element $x_{9}$ och $x_{10}$ av $M$, så att $\divides {x_{9}}{\mathrm{\_a}}$, $\divides {x_{10}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{x_{9} \times x_{10}}$.ifI 21 [dvd]
23.För alla element $\mathrm{\_b}$ av $M$, om $\divides {p}{\mathrm{\_a} \times \mathrm{\_b}}$, så finns det element $x_{11}$ och $x_{12}$ av $M$, så att $\divides {x_{11}}{\mathrm{\_a}}$, $\divides {x_{12}}{\mathrm{\_b}}$ och $\EqtMACRoJ {p}{x_{11} \times x_{12}}$.forallI 1, 22 [_b]
24.För alla element $\mathrm{\_a}$ och $\mathrm{\_b1}$ av $M$, om $\divides {p}{\mathrm{\_a} \times \mathrm{\_b1}}$, så finns det element $x_{13}$ och $x_{14}$ av $M$, så att $\divides {x_{13}}{\mathrm{\_a}}$, $\divides {x_{14}}{\mathrm{\_b1}}$ och $\EqtMACRoJ {p}{x_{13} \times x_{14}}$.forallI 1, 23 [_a]
Prime.not_dvd_multheoremDefs.lean:74
Lean
theorem not_dvd_mul {a b : M} (ha : ¬ p ∣ a) (hb : ¬ p ∣ b) : ¬ p ∣ a * b :=
  hp.dvd_mul.not.mpr <| not_or.mpr ⟨ha, hb⟩
Dedukti
2 lines
def Prime__not_dvd_mul : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> (a : Elem M) -> (b : Elem M) -> (ha : Proof (not (divide p a))) -> (hb : Proof (not (divide p b))) -> Proof (not (divide p (times a b))) :=
  M => x => p => hp => a => b => ha => hb => iffEr (not (divide p (times a b))) (not (or (divide p a) (divide p b))) (Iff__not (divide p (times a b)) (or (divide p a) (divide p b)) (Prime__dvd_mul M p hp a b)) (iffEr (not (or (divide p a) (divide p b))) (and (not (divide p a)) (not (divide p b))) (not_or (divide p a) (divide p b)) (andI (not (divide p a)) (not (divide p b)) ha hb)).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$, $a$ and $b$ be elements of $M$ such that $p$ is prime, $p$ does not divide $a$ and $p$ does not divide $b$. Then $p$ does not divide $a \times b$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soient $p$, $a$ et $b$ des éléments de $M$ tels que $p$ soit premier, $p$ ne divise pas $a$ et $p$ ne divise pas $b$. Alors $p$ ne divise pas $a \times b$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$, $a$ a $b$ je prvek $M$ takový, že $p$ je prvočíselné, $p$ nedělí $a$ a $p$ nedělí $b$. Tedy $p$ nedělí $a \times b$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Seien $p$, $a$ und $b$ elemente von $M$ derart, dass ist $p$ prim, $p$ nicht $a$ teilt und $p$ nicht $b$ teilt. Dann teilt $p$ nicht $a \times b$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$, $a$ och $b$ vara element av $M$ sådana att $p$ är primt, $p$ inte delar $a$ och $p$ inte delar $b$. Då delar $p$ inte $a \times b$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p), a , b \in M , \neg (\divides {p}{a}), \neg (\divides {p}{b})\vdash \neg (\divides {p}{a \times b})$
Proof
10 lines
1.Let $p$, $a$ and $b$ be elements of $M$.
2.Assume that $p$ is prime.
3.$\divides {p}{a \times b}$, if and only if $\divides {p}{a}$ or $\divides {p}{b}$.Prime.dvd_mul 2
4.It is not the case that $\divides {p}{a \times b}$, if and only if it is not the case that $\divides {p}{a}$ or $\divides {p}{b}$.Iff.not 3
5.It is not the case that $\divides {p}{a}$ or $\divides {p}{b}$, if and only if it is not the case that $\divides {p}{a}$ and it is not the case that $\divides {p}{b}$.not_or
6.Assume that it is not the case that $\divides {p}{a}$.
7.Assume that it is not the case that $\divides {p}{b}$.
8.It is not the case that $\divides {p}{a}$ and it is not the case that $\divides {p}{b}$.andI 6, 7
9.It is not the case that $\divides {p}{a}$ or $\divides {p}{b}$.iffEr 5, 8
10.It is not the case that $\divides {p}{a \times b}$.iffEr 4, 9
Proof, French
10 lines
1.Soient $p$, $a$ et $b$ des éléments de $M$.
2.Supposons que $p$ est premier.
3.$\divides {p}{a \times b}$ si et seulement si $\divides {p}{a}$ ou $\divides {p}{b}$.Prime.dvd_mul 2
4.Il n'est pas le cas que $\divides {p}{a \times b}$ si et seulement si il n'est pas le cas que $\divides {p}{a}$ ou $\divides {p}{b}$.Iff.not 3
5.Il n'est pas le cas que $\divides {p}{a}$ ou $\divides {p}{b}$ si et seulement si il n'est pas le cas que $\divides {p}{a}$ et il n'est pas le cas que $\divides {p}{b}$.not_or
6.Supposons qu'il n'est pas le cas que $\divides {p}{a}$.
7.Supposons qu'il n'est pas le cas que $\divides {p}{b}$.
8.Il n'est pas le cas que $\divides {p}{a}$ et il n'est pas le cas que $\divides {p}{b}$.andI 6, 7
9.Il n'est pas le cas que $\divides {p}{a}$ ou $\divides {p}{b}$.iffEr 5, 8
10.Il n'est pas le cas que $\divides {p}{a \times b}$.iffEr 4, 9
Proof, Czech
10 lines
1.Nechť $p$, $a$ a $b$ je prvek $M$.
2.Předpokládejme, že $p$ je prvočíselné.
3.$\divides {p}{a \times b}$, právě tehdy, když $\divides {p}{a}$ nebo $\divides {p}{b}$.Prime.dvd_mul 2
4.Není případ že $\divides {p}{a \times b}$, právě tehdy, když není případ že $\divides {p}{a}$ nebo $\divides {p}{b}$.Iff.not 3
5.Není případ že $\divides {p}{a}$ nebo $\divides {p}{b}$, právě tehdy, když není případ že $\divides {p}{a}$ a není případ že $\divides {p}{b}$.not_or
6.Předpokládejme, že není případ že $\divides {p}{a}$.
7.Předpokládejme, že není případ že $\divides {p}{b}$.
8.Není případ že $\divides {p}{a}$ a není případ že $\divides {p}{b}$.andI 6, 7
9.Není případ že $\divides {p}{a}$ nebo $\divides {p}{b}$.iffEr 5, 8
10.Není případ že $\divides {p}{a \times b}$.iffEr 4, 9
Proof, German
10 lines
1.Seien $p$, $a$ und $b$ elemente von $M$.
2.Nimm an, dass $p$ prim ist.
3.$\divides {p}{a \times b}$, genau dann, wenn $\divides {p}{a}$ oder $\divides {p}{b}$.Prime.dvd_mul 2
4.Es ist nicht der Fall dass $\divides {p}{a \times b}$, genau dann, wenn es nicht der Fall dass $\divides {p}{a}$ oder $\divides {p}{b}$ ist.Iff.not 3
5.Es ist nicht der Fall dass $\divides {p}{a}$ oder $\divides {p}{b}$, genau dann, wenn es nicht der Fall dass $\divides {p}{a}$ ist und es nicht der Fall dass $\divides {p}{b}$ ist.not_or
6.Nimm an, dass es nicht der Fall dass $\divides {p}{a}$ ist.
7.Nimm an, dass es nicht der Fall dass $\divides {p}{b}$ ist.
8.Es ist nicht der Fall dass $\divides {p}{a}$ und es ist nicht der Fall dass $\divides {p}{b}$.andI 6, 7
9.Es ist nicht der Fall dass $\divides {p}{a}$ oder $\divides {p}{b}$.iffEr 5, 8
10.Es ist nicht der Fall dass $\divides {p}{a \times b}$.iffEr 4, 9
Proof, Swedish
10 lines
1.Låt $p$, $a$ och $b$ vara element av $M$.
2.Anta att $p$ är primt.
3.$\divides {p}{a \times b}$, om och endast om $\divides {p}{a}$ eller $\divides {p}{b}$.Prime.dvd_mul 2
4.Det är inte fallet att $\divides {p}{a \times b}$, om och endast om det inte är fallet att $\divides {p}{a}$ eller $\divides {p}{b}$.Iff.not 3
5.Det är inte fallet att $\divides {p}{a}$ eller $\divides {p}{b}$, om och endast om det inte är fallet att $\divides {p}{a}$ och det inte är fallet att $\divides {p}{b}$.not_or
6.Anta att det inte är fallet att $\divides {p}{a}$.
7.Anta att det inte är fallet att $\divides {p}{b}$.
8.Det är inte fallet att $\divides {p}{a}$ och det är inte fallet att $\divides {p}{b}$.andI 6, 7
9.Det är inte fallet att $\divides {p}{a}$ eller $\divides {p}{b}$.iffEr 5, 8
10.Det är inte fallet att $\divides {p}{a \times b}$.iffEr 4, 9
Prime.dvd_of_dvd_powtheoremDefs.lean:77
Lean
theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a :=
Dedukti
1 lines
Prime__dvd_of_dvd_pow : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> (a : Elem M) -> (n : Elem Nat) -> (h : Proof (divide p (pow a n))) -> Proof (divide p a).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ and $a$ be elements of $M$ such that $p$ is prime. Let $n$ be a natural number such that $p$ divides $a ^ {n}$. Then $p$ divides $a$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soient $p$ et $a$ des éléments de $M$ tels que $p$ soit premier. Soit $n$ un nombre naturel tel que $p$ divise $a ^ {n}$. Alors $p$ divise $a$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ a $a$ je prvek $M$ takový, že $p$ je prvočíselné. Nechť $n$ je přirozené číslo takové, že $p$ dělí $a ^ {n}$. Tedy $p$ dělí $a$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Seien $p$ und $a$ elemente von $M$ derart, dass $p$ prim ist. Sei $n$ eine natürliche Zahl derart, dass $p$ $a ^ {n}$ teilt. Dann teilt $p$ $a$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ och $a$ vara element av $M$ sådana att $p$ är primt. Låt $n$ vara ett naturligt tal sådant att $p$ delar $a ^ {n}$. Då delar $p$ $a$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p), a \in M , n \in \Natural , \divides {p}{a ^ {n}}\vdash \divides {p}{a}$
Prime.dvd_pow_iff_dvdtheoremDefs.lean:90
Lean
theorem dvd_pow_iff_dvd {a : M} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a :=
  ⟨hp.dvd_of_dvd_pow, (dvd_pow · hn)⟩
Dedukti
2 lines
def Prime__dvd_pow_iff_dvd : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> (a : Elem M) -> (n : Elem Nat) -> (hn : Proof (Neq n 0)) -> Proof (iff (divide p (pow a n)) (divide p a)) :=
  M => x => p => hp => a => n => hn => iffI (divide p (pow a n)) (divide p a) (Prime__dvd_of_dvd_pow M p hp a n) (h => dvd_pow M p a h n hn).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $p$ and $a$ be elements of $M$ such that $p$ is prime. Let $n$ be a natural number such that $n \neq 0$. Then $p$ divides $a ^ {n}$, if and only if $p$ divides $a$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soient $p$ et $a$ des éléments de $M$ tels que $p$ soit premier. Soit $n$ un nombre naturel tel que $n \neq 0$. Alors $p$ divise $a ^ {n}$ si et seulement si $p$ divise $a$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $p$ a $a$ je prvek $M$ takový, že $p$ je prvočíselné. Nechť $n$ je přirozené číslo takové, že $n \neq 0$. Tedy $p$ dělí $a ^ {n}$, právě tehdy, když $p$ dělí $a$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Seien $p$ und $a$ elemente von $M$ derart, dass $p$ prim ist. Sei $n$ eine natürliche Zahl derart, dass $n \neq 0$. Dann teilt $p$ $a ^ {n}$, genau dann, wenn $p$ $a$ teilt.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $p$ och $a$ vara element av $M$ sådana att $p$ är primt. Låt $n$ vara ett naturligt tal sådant att $n \neq 0$. Då delar $p$ $a ^ {n}$, om och endast om $p$ delar $a$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), p \in M , \mathrm{Prime} (p), a \in M , n \in \Natural , n \neq 0 \vdash \divides {p}{a ^ {n}}\leftrightarrow \divides {p}{a}$
Proof
8 lines
1.Let $p$ and $a$ be elements of $M$.
2.Let $n$ be an element of $\Natural$.
3.Assume that $p$ is prime.
4.$\divides {p}{a}$.Prime.dvd_of_dvd_pow 3
5.Assume that $\divides {p}{a}$.
6.Assume that $n \neq 0$.
7.$\divides {p}{a ^ {n}}$.dvd_pow 5, 6
8.$\divides {p}{a ^ {n}}$, if and only if $\divides {p}{a}$.iffI 4, 7 [h]
Proof, French
8 lines
1.Soient $p$ et $a$ des éléments de $M$.
2.Soit $n$ un élément de $\Natural$.
3.Supposons que $p$ est premier.
4.$\divides {p}{a}$.Prime.dvd_of_dvd_pow 3
5.Supposons que $\divides {p}{a}$.
6.Supposons que $n \neq 0$.
7.$\divides {p}{a ^ {n}}$.dvd_pow 5, 6
8.$\divides {p}{a ^ {n}}$ si et seulement si $\divides {p}{a}$.iffI 4, 7 [h]
Proof, Czech
8 lines
1.Nechť $p$ a $a$ je prvek $M$.
2.Nechť $n$ je prvek $\Natural$.
3.Předpokládejme, že $p$ je prvočíselné.
4.$\divides {p}{a}$.Prime.dvd_of_dvd_pow 3
5.Předpokládejme, že $\divides {p}{a}$.
6.Předpokládejme, že $n \neq 0$.
7.$\divides {p}{a ^ {n}}$.dvd_pow 5, 6
8.$\divides {p}{a ^ {n}}$, právě tehdy, když $\divides {p}{a}$.iffI 4, 7 [h]
Proof, German
8 lines
1.Seien $p$ und $a$ elemente von $M$.
2.Sei $n$ ein Element von $\Natural$.
3.Nimm an, dass $p$ prim ist.
4.$\divides {p}{a}$.Prime.dvd_of_dvd_pow 3
5.Nimm an, dass $\divides {p}{a}$.
6.Nimm an, dass $n \neq 0$.
7.$\divides {p}{a ^ {n}}$.dvd_pow 5, 6
8.$\divides {p}{a ^ {n}}$, genau dann, wenn $\divides {p}{a}$.iffI 4, 7 [h]
Proof, Swedish
8 lines
1.Låt $p$ och $a$ vara element av $M$.
2.Låt $n$ vara ett element av $\Natural$.
3.Anta att $p$ är primt.
4.$\divides {p}{a}$.Prime.dvd_of_dvd_pow 3
5.Anta att $\divides {p}{a}$.
6.Anta att $n \neq 0$.
7.$\divides {p}{a ^ {n}}$.dvd_pow 5, 6
8.$\divides {p}{a ^ {n}}$, om och endast om $\divides {p}{a}$.iffI 4, 7 [h]
not_prime_zerotheoremDefs.lean:96
Lean
@[simp]
theorem not_prime_zero : ¬Prime (0 : M) := fun h => h.ne_zero rfl
Dedukti
2 lines
def not_prime_zero : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> Proof (not (Prime 0)) :=
  M => x => ifI (Prime 0) false (h => Prime__ne_zero M 0 h rfl).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Then $0$ is not prime.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Alors $0$ n'est pas premier.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Tedy $0$ není prvočíselné.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Dann ist $0$ nicht prim.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Då är $0$ inte primt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M)\vdash \neg \mathrm{Prime} (0)$
Proof
3 lines
1.Assume that $0$ is prime.
2.$0 \neq 0$.Prime.ne_zero 1
3.If $0$ is prime, then we have a contradiction.ifI 2 [h]
Proof, French
3 lines
1.Supposons que $0$ est premier.
2.$0 \neq 0$.Prime.ne_zero 1
3.Si $0$ est premier, alors nous avons une contradiction.ifI 2 [h]
Proof, Czech
3 lines
1.Předpokládejme, že $0$ je prvočíselné.
2.$0 \neq 0$.Prime.ne_zero 1
3.Jestliže $0$ je prvočíselné, pak máme spor.ifI 2 [h]
Proof, German
3 lines
1.Nimm an, dass $0$ prim ist.
2.$0 \neq 0$.Prime.ne_zero 1
3.Wenn $0$ prim ist, dann haben wir einen Widerspruch.ifI 2 [h]
Proof, Swedish
3 lines
1.Anta att $0$ är primt.
2.$0 \neq 0$.Prime.ne_zero 1
3.Om $0$ är primt, så har vi en kontradiction.ifI 2 [h]
not_prime_onetheoremDefs.lean:99
Lean
@[simp]
theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_isUnit isUnit_one
Dedukti
2 lines
def not_prime_one : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> Proof (not (Prime 1)) :=
  M => x => ifI (Prime 1) false (h => Prime__not_isUnit M 1 h (isUnit_one M)).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Then $1$ is not prime.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Alors $1$ n'est pas premier.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Tedy $1$ není prvočíselné.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Dann ist $1$ nicht prim.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Då är $1$ inte primt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M)\vdash \neg \mathrm{Prime} (1)$
Proof
3 lines
1.Assume that $1$ is prime.
2.$1$ is not a unit.Prime.not_isUnit 1
3.If $1$ is prime, then we have a contradiction.ifI 2 [h]
Proof, French
3 lines
1.Supposons que $1$ est premier.
2.$1$ n'est pas une unité.Prime.not_isUnit 1
3.Si $1$ est premier, alors nous avons une contradiction.ifI 2 [h]
Proof, Czech
3 lines
1.Předpokládejme, že $1$ je prvočíselné.
2.$1$ není jednotka.Prime.not_isUnit 1
3.Jestliže $1$ je prvočíselné, pak máme spor.ifI 2 [h]
Proof, German
3 lines
1.Nimm an, dass $1$ prim ist.
2.$1$ ist nicht eine Einheit.Prime.not_isUnit 1
3.Wenn $1$ prim ist, dann haben wir einen Widerspruch.ifI 2 [h]
Proof, Swedish
3 lines
1.Anta att $1$ är primt.
2.$1$ är inte en enhet.Prime.not_isUnit 1
3.Om $1$ är primt, så har vi en kontradiction.ifI 2 [h]
Irreducible.not_dvd_isUnittheoremDefs.lean:103
Lean
theorem Irreducible.not_dvd_isUnit [CommMonoid M] {p u : M} (hp : Irreducible p) (hu : IsUnit u) :
    ¬p ∣ u :=
  mt (isUnit_of_dvd_unit · hu) hp.not_isUnit
Dedukti
2 lines
def Irreducible__not_dvd_isUnit : (M : Set) -> (_ : Proof (CommMonoid M)) -> (p : Elem M) -> (u : Elem M) -> (hp : Proof (Irreducible p)) -> (hu : Proof (IsUnit u)) -> Proof (not (divide p u)) :=
  M => x => p => u => hp => hu => mt (divide p u) (IsUnit p) (ifI (divide p u) (IsUnit p) (h => isUnit_of_dvd_unit M p u h hu)) (Irreducible__not_isUnit M p hp).
English
Let $M$ be a set such that $M$ is a commutative monoid. Let $p$ and $u$ be elements of $M$ such that $p$ is irreducible and $u$ is a unit. Then $p$ does not divide $u$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde commutatif. Soient $p$ et $u$ des éléments de $M$ tels que $p$ soit irréductible et $u$ soit une unité. Alors $p$ ne divise pas $u$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid. Nechť $p$ a $u$ je prvek $M$ takový, že $p$ je ireducibilní a $u$ je jednotka. Tedy $p$ nedělí $u$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid ist. Seien $p$ und $u$ elemente von $M$ derart, dass $p$ irreduzibl ist und $u$ eine Einheit ist. Dann teilt $p$ nicht $u$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid. Låt $p$ och $u$ vara element av $M$ sådana att $p$ är irreducibelt och $u$ är en enhet. Då delar $p$ inte $u$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoid} (M), p , u \in M , \mathrm{Irreducible} (p), \mathrm{IsUnit} (u)\vdash \neg (\divides {p}{u})$
Proof
8 lines
1.Let $p$ and $u$ be elements of $M$.
2.Assume that $\divides {p}{u}$.
3.Assume that $u$ is a unit.
4.$p$ is a unit.isUnit_of_dvd_unit 2, 3
5.If $\divides {p}{u}$, then $p$ is a unit.ifI 4 [h]
6.Assume that $p$ is irreducible.
7.$p$ is not a unit.Irreducible.not_isUnit 6
8.It is not the case that $\divides {p}{u}$.mt 5, 7
Proof, French
8 lines
1.Soient $p$ et $u$ des éléments de $M$.
2.Supposons que $\divides {p}{u}$.
3.Supposons que $u$ est une unité.
4.$p$ est une unité.isUnit_of_dvd_unit 2, 3
5.Si $\divides {p}{u}$, alors $p$ est une unité.ifI 4 [h]
6.Supposons que $p$ est irréductible.
7.$p$ n'est pas une unité.Irreducible.not_isUnit 6
8.Il n'est pas le cas que $\divides {p}{u}$.mt 5, 7
Proof, Czech
8 lines
1.Nechť $p$ a $u$ je prvek $M$.
2.Předpokládejme, že $\divides {p}{u}$.
3.Předpokládejme, že $u$ je jednotka.
4.$p$ je jednotka.isUnit_of_dvd_unit 2, 3
5.Jestliže $\divides {p}{u}$, pak $p$ je jednotka.ifI 4 [h]
6.Předpokládejme, že $p$ je ireducibilní.
7.$p$ není jednotka.Irreducible.not_isUnit 6
8.Není případ že $\divides {p}{u}$.mt 5, 7
Proof, German
8 lines
1.Seien $p$ und $u$ elemente von $M$.
2.Nimm an, dass $\divides {p}{u}$.
3.Nimm an, dass $u$ eine Einheit ist.
4.$p$ ist eine Einheit.isUnit_of_dvd_unit 2, 3
5.Wenn $\divides {p}{u}$, dann ist $p$ eine Einheit.ifI 4 [h]
6.Nimm an, dass $p$ irreduzibl ist.
7.$p$ ist nicht eine Einheit.Irreducible.not_isUnit 6
8.Es ist nicht der Fall dass $\divides {p}{u}$.mt 5, 7
Proof, Swedish
8 lines
1.Låt $p$ och $u$ vara element av $M$.
2.Anta att $\divides {p}{u}$.
3.Anta att $u$ är en enhet.
4.$p$ är en enhet.isUnit_of_dvd_unit 2, 3
5.Om $\divides {p}{u}$, så är $p$ en enhet.ifI 4 [h]
6.Anta att $p$ är irreducibelt.
7.$p$ är inte en enhet.Irreducible.not_isUnit 6
8.Det är inte fallet att $\divides {p}{u}$.mt 5, 7
Irreducible.not_dvd_onetheoremDefs.lean:107
Lean
theorem Irreducible.not_dvd_one [CommMonoid M] {p : M} (hp : Irreducible p) : ¬p ∣ 1 :=
  hp.not_dvd_isUnit isUnit_one
Dedukti
2 lines
def Irreducible__not_dvd_one : (M : Set) -> (_ : Proof (CommMonoid M)) -> (p : Elem M) -> (hp : Proof (Irreducible p)) -> Proof (not (divide p 1)) :=
  M => x => p => hp => Irreducible__not_dvd_isUnit M p 1 hp (isUnit_one M).
English
Let $M$ be a set such that $M$ is a commutative monoid. Let $p$ be an irreducible element of $M$. Then $p$ does not divide $1$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde commutatif. Soit $p$ un élément de $M$ irréductible. Alors $p$ ne divise pas $1$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid. Nechť $p$ je ireducibilní prvek $M$. Tedy $p$ nedělí $1$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid ist. Sei $p$ ein irreduzibles Element von $M$. Dann teilt $p$ nicht $1$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid. Låt $p$ vara ett irreducibelt element av $M$. Då delar $p$ inte $1$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoid} (M), p \in M , \mathrm{Irreducible} (p)\vdash \neg (\divides {p}{1})$
Proof
4 lines
1.Let $p$ be an element of $M$.
2.Assume that $p$ is irreducible.
3.$1$ is a unit.isUnit_one
4.It is not the case that $\divides {p}{1}$.Irreducible.not_dvd_isUnit 2, 3
Proof, French
4 lines
1.Soit $p$ un élément de $M$.
2.Supposons que $p$ est irréductible.
3.$1$ est une unité.isUnit_one
4.Il n'est pas le cas que $\divides {p}{1}$.Irreducible.not_dvd_isUnit 2, 3
Proof, Czech
4 lines
1.Nechť $p$ je prvek $M$.
2.Předpokládejme, že $p$ je ireducibilní.
3.$1$ je jednotka.isUnit_one
4.Není případ že $\divides {p}{1}$.Irreducible.not_dvd_isUnit 2, 3
Proof, German
4 lines
1.Sei $p$ ein Element von $M$.
2.Nimm an, dass $p$ irreduzibl ist.
3.$1$ ist eine Einheit.isUnit_one
4.Es ist nicht der Fall dass $\divides {p}{1}$.Irreducible.not_dvd_isUnit 2, 3
Proof, Swedish
4 lines
1.Låt $p$ vara ett element av $M$.
2.Anta att $p$ är irreducibelt.
3.$1$ är en enhet.isUnit_one
4.Det är inte fallet att $\divides {p}{1}$.Irreducible.not_dvd_isUnit 2, 3
Irreducible.not_dvd_unittheoremDefs.lean:110
Lean
theorem Irreducible.not_dvd_unit [CommMonoid M] {p : M} (u : Mˣ) (hp : Irreducible p) :
    ¬ p ∣ u :=
  hp.not_dvd_isUnit u.isUnit
Dedukti
2 lines
def Irreducible__not_dvd_unit : (M : Set) -> (_ : Proof (CommMonoid M)) -> (p : Elem M) -> (u : Elem (Units M)) -> (hp : Proof (Irreducible p)) -> Proof (not (divide p (Units__val u))) :=
  M => x => p => u => hp => Irreducible__not_dvd_isUnit M p (Units__val u) hp (Units__isUnit M u).
English
Let $M$ be a set such that $M$ is a commutative monoid. Let $p$ be an element of $M$. Let $u$ be a unit of $M$. Assume that $p$ is irreducible. Then $p$ does not divide the underlying value in the base of $u$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde commutatif. Soit $p$ un élément de $M$. Soit $u$ une unité de $M$. Supposons que $p$ est irréductible. Alors $p$ ne divise pas le [DepNoun] sous-jacent de $u$.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid. Nechť $p$ je prvek $M$. Nechť $u$ je jednotka $M$. Předpokládejme, že $p$ je ireducibilní. Tedy $p$ nedělí podkladového [DepNoun] $u$.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid ist. Sei $p$ ein Element von $M$. Sei $u$ eine Einheit von $M$. Nimm an, dass $p$ irreduzibl ist. Dann teilt $p$ nicht $\operatorname{val}$ angewandt auf $u$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid. Låt $p$ vara ett element av $M$. Låt $u$ vara en enhet av $M$. Anta att $p$ är irreducibelt. Då delar $p$ inte $\operatorname{val}$ applicerat på $u$.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoid} (M), p \in M , u \in \UnitsMACRoAX {M}, \mathrm{Irreducible} (p)\vdash \neg (\divides {p}{\operatorname{val} (u)})$
Proof
5 lines
1.Let $p$ be an element of $M$.
2.Let $u$ be an element of $\UnitsMACRoAX {M}$.
3.Assume that $p$ is irreducible.
4.The underlying value in the base of $u$ is a unit.Units.isUnit
5.$p$ does not divide the underlying value in the base of $u$.Irreducible.not_dvd_isUnit 3, 4
Proof, French
5 lines
1.Soit $p$ un élément de $M$.
2.Soit $u$ un élément de $\UnitsMACRoAX {M}$.
3.Supposons que $p$ est irréductible.
4.Le [DepNoun] sous-jacent de $u$ est une unité.Units.isUnit
5.$p$ ne divise pas le [DepNoun] sous-jacent de $u$.Irreducible.not_dvd_isUnit 3, 4
Proof, Czech
5 lines
1.Nechť $p$ je prvek $M$.
2.Nechť $u$ je prvek $\UnitsMACRoAX {M}$.
3.Předpokládejme, že $p$ je ireducibilní.
4.Podkladový [DepNoun] $u$ je jednotka.Units.isUnit
5.$p$ nedělí podkladového [DepNoun] $u$.Irreducible.not_dvd_isUnit 3, 4
Proof, German
5 lines
1.Sei $p$ ein Element von $M$.
2.Sei $u$ ein Element von $\UnitsMACRoAX {M}$.
3.Nimm an, dass $p$ irreduzibl ist.
4.Units.isUnit
5.Irreducible.not_dvd_isUnit 3, 4
Proof, Swedish
5 lines
1.Låt $p$ vara ett element av $M$.
2.Låt $u$ vara ett element av $\UnitsMACRoAX {M}$.
3.Anta att $p$ är irreducibelt.
4.$\operatorname{val}$ applicerat på $u$ är en enhet.Units.isUnit
5.Det är inte fallet att $\divides {p}{\operatorname{val} (u)}$.Irreducible.not_dvd_isUnit 3, 4
Irreducible.isUnit_of_mul_self_dvdtheoremDefs.lean:114
Lean
theorem Irreducible.isUnit_of_mul_self_dvd [CommMonoid M] {p a : M} (hp : Irreducible p)
    (ha : a * a ∣ p) : IsUnit a :=
Dedukti
1 lines
Irreducible__isUnit_of_mul_self_dvd : (M : Set) -> (_ : Proof (CommMonoid M)) -> (p : Elem M) -> (a : Elem M) -> (hp : Proof (Irreducible p)) -> (ha : Proof (divide (times a a) p)) -> Proof (IsUnit a).
English
Let $M$ be a set such that $M$ is a commutative monoid. Let $p$ and $a$ be elements of $M$ such that $p$ is irreducible and $a \times a$ divides $p$. Then $a$ is a unit.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde commutatif. Soient $p$ et $a$ des éléments de $M$ tels que $p$ soit irréductible et $a \times a$ divise $p$. Alors $a$ est une unité.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid. Nechť $p$ a $a$ je prvek $M$ takový, že $p$ je ireducibilní a $a \times a$ dělí $p$. Tedy $a$ je jednotka.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid ist. Seien $p$ und $a$ elemente von $M$ derart, dass $p$ irreduzibl ist und $a \times a$ $p$ teilt. Dann ist $a$ eine Einheit.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid. Låt $p$ och $a$ vara element av $M$ sådana att $p$ är irreducibelt och $a \times a$ delar $p$. Då är $a$ en enhet.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoid} (M), p , a \in M , \mathrm{Irreducible} (p), \divides {a \times a}{p}\vdash \mathrm{IsUnit} (a)$
not_irreducible_zerotheoremDefs.lean:122
Lean
@[simp]
theorem not_irreducible_zero [MonoidWithZero M] : ¬Irreducible (0 : M)
Dedukti
1 lines
not_irreducible_zero : (M : Set) -> (_ : Proof (MonoidWithZero M)) -> Proof (not (Irreducible 0)).
English
Let $M$ be a set such that $M$ is a monoid with zero. Then $0$ is not irreducible.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro. Alors $0$ n'est pas irréductible.
Czech
Nechť $M$ je množina taková, že $M$ je monoid s nulou. Tedy $0$ není ireducibilní.
German
Sei $M$ eine Menge derart, dass $M$ ein Monoid mit Null ist. Dann ist $0$ nicht irreduzibl.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en monoid med nolla. Då är $0$ inte irreducibelt.
Formula
$M \in \mathrm{Set} , \mathrm{MonoidWithZero} (M)\vdash \neg \mathrm{Irreducible} (0)$
Irreducible.ne_zerotheoremDefs.lean:127
Lean
theorem Irreducible.ne_zero [MonoidWithZero M] : ∀ {p : M}, Irreducible p → p ≠ 0
Dedukti
1 lines
Irreducible__ne_zero : (M : Set) -> (_ : Proof (MonoidWithZero M)) -> (p : Elem M) -> (h : Proof (Irreducible p)) -> Proof (Neq p 0).
English
Let $M$ be a set such that $M$ is a monoid with zero. Let $p$ be an irreducible element of $M$. Then $p \neq 0$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro. Soit $p$ un élément de $M$ irréductible. Alors $p \neq 0$.
Czech
Nechť $M$ je množina taková, že $M$ je monoid s nulou. Nechť $p$ je ireducibilní prvek $M$. Tedy $p \neq 0$.
German
Sei $M$ eine Menge derart, dass $M$ ein Monoid mit Null ist. Sei $p$ ein irreduzibles Element von $M$. Dann $p \neq 0$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en monoid med nolla. Låt $p$ vara ett irreducibelt element av $M$. Då $p \neq 0$.
Formula
$M \in \mathrm{Set} , \mathrm{MonoidWithZero} (M), p \in M , \mathrm{Irreducible} (p)\vdash p \neq 0$
Irreducible.dvd_symmtheoremDefs.lean:131
If p and q are irreducible, then p ∣ q implies q ∣ p.
Lean
theorem Irreducible.dvd_symm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
    p ∣ q → q ∣ p :=
Dedukti
1 lines
Irreducible__dvd_symm : (M : Set) -> (_ : Proof (Monoid M)) -> (p : Elem M) -> (q : Elem M) -> (hp : Proof (Irreducible p)) -> (hq : Proof (Irreducible q)) -> (h : Proof (divide p q)) -> Proof (divide q p).
English
Let $M$ be a set such that $M$ is a monoid. Let $p$ and $q$ be elements of $M$ such that $p$ and $q$ are irreducible and $p$ divides $q$. Then $q$ divides $p$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde. Soient $p$ et $q$ des éléments de $M$ tels que $p$ et $q$ soient irréductibles et $p$ divise $q$. Alors $q$ divise $p$.
Czech
Nechť $M$ je množina taková, že $M$ je monoid. Nechť $p$ a $q$ je prvek $M$ takový, že $p$ a $q$ je ireducibilní a $p$ dělí $q$. Tedy $q$ dělí $p$.
German
Sei $M$ eine Menge derart, dass $M$ ein Monoid ist. Seien $p$ und $q$ elemente von $M$ derart, dass sowohl $p$ als auch $q$ irreduzibl ist und $p$ $q$ teilt. Dann teilt $q$ $p$.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en monoid. Låt $p$ och $q$ vara element av $M$ sådana att $p$ och $q$ är irreducibla och $p$ delar $q$. Då delar $q$ $p$.
Formula
$M \in \mathrm{Set} , \mathrm{Monoid} (M), p , q \in M , \mathrm{Irreducible} (p), \mathrm{Irreducible} (q), \divides {p}{q}\vdash \divides {q}{p}$
Irreducible.dvd_commtheoremDefs.lean:136
Lean
theorem Irreducible.dvd_comm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
    p ∣ q ↔ q ∣ p :=
  ⟨hp.dvd_symm hq, hq.dvd_symm hp⟩
Dedukti
2 lines
def Irreducible__dvd_comm : (M : Set) -> (_ : Proof (Monoid M)) -> (p : Elem M) -> (q : Elem M) -> (hp : Proof (Irreducible p)) -> (hq : Proof (Irreducible q)) -> Proof (iff (divide p q) (divide q p)) :=
  M => x => p => q => hp => hq => iffI (divide p q) (divide q p) (Irreducible__dvd_symm M p q hp hq) (Irreducible__dvd_symm M q p hq hp).
English
Let $M$ be a set such that $M$ is a monoid. Let $p$ and $q$ be irreducible elements of $M$. Then $p$ divides $q$, if and only if $q$ divides $p$.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde. Soient $p$ et $q$ des éléments de $M$ irréductibles. Alors $p$ divise $q$ si et seulement si $q$ divise $p$.
Czech
Nechť $M$ je množina taková, že $M$ je monoid. Nechť $p$ a $q$ je ireducibilní prvek $M$. Tedy $p$ dělí $q$, právě tehdy, když $q$ dělí $p$.
German
Sei $M$ eine Menge derart, dass $M$ ein Monoid ist. Seien $p$ und $q$ irreduzible Elemente von $M$. Dann teilt $p$ $q$, genau dann, wenn $q$ $p$ teilt.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en monoid. Låt $p$ och $q$ vara irreducibla element av $M$. Då delar $p$ $q$, om och endast om $q$ delar $p$.
Formula
$M \in \mathrm{Set} , \mathrm{Monoid} (M), p , q \in M , \mathrm{Irreducible} (p), \mathrm{Irreducible} (q)\vdash \divides {p}{q}\leftrightarrow \divides {q}{p}$
Proof
6 lines
1.Let $p$ and $q$ be elements of $M$.
2.Assume that $p$ is irreducible.
3.Assume that $q$ is irreducible.
4.$\divides {q}{p}$.Irreducible.dvd_symm 2, 3
5.$\divides {p}{q}$.Irreducible.dvd_symm 3, 2
6.$\divides {p}{q}$, if and only if $\divides {q}{p}$.iffI 4, 5
Proof, French
6 lines
1.Soient $p$ et $q$ des éléments de $M$.
2.Supposons que $p$ est irréductible.
3.Supposons que $q$ est irréductible.
4.$\divides {q}{p}$.Irreducible.dvd_symm 2, 3
5.$\divides {p}{q}$.Irreducible.dvd_symm 3, 2
6.$\divides {p}{q}$ si et seulement si $\divides {q}{p}$.iffI 4, 5
Proof, Czech
6 lines
1.Nechť $p$ a $q$ je prvek $M$.
2.Předpokládejme, že $p$ je ireducibilní.
3.Předpokládejme, že $q$ je ireducibilní.
4.$\divides {q}{p}$.Irreducible.dvd_symm 2, 3
5.$\divides {p}{q}$.Irreducible.dvd_symm 3, 2
6.$\divides {p}{q}$, právě tehdy, když $\divides {q}{p}$.iffI 4, 5
Proof, German
6 lines
1.Seien $p$ und $q$ elemente von $M$.
2.Nimm an, dass $p$ irreduzibl ist.
3.Nimm an, dass $q$ irreduzibl ist.
4.$\divides {q}{p}$.Irreducible.dvd_symm 2, 3
5.$\divides {p}{q}$.Irreducible.dvd_symm 3, 2
6.$\divides {p}{q}$, genau dann, wenn $\divides {q}{p}$.iffI 4, 5
Proof, Swedish
6 lines
1.Låt $p$ och $q$ vara element av $M$.
2.Anta att $p$ är irreducibelt.
3.Anta att $q$ är irreducibelt.
4.$\divides {q}{p}$.Irreducible.dvd_symm 2, 3
5.$\divides {p}{q}$.Irreducible.dvd_symm 3, 2
6.$\divides {p}{q}$, om och endast om $\divides {q}{p}$.iffI 4, 5
Irreducible.prime_of_isPrimaltheoremDefs.lean:144
Lean
theorem Irreducible.prime_of_isPrimal {a : M}
    (irr : Irreducible a) (primal : IsPrimal a) : Prime a :=
Dedukti
1 lines
Irreducible__prime_of_isPrimal : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (a : Elem M) -> (irr : Proof (Irreducible a)) -> (primal : Proof (IsPrimal a)) -> Proof (Prime a).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero. Let $a$ be an element of $M$ such that $a$ is irreducible and primal. Then $a$ is prime.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif. Soit $a$ un élément de $M$ tel que $a$ soit irréductible et primal. Alors $a$ est premier.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou. Nechť $a$ je prvek $M$ takový, že $a$ je ireducibilní a prvotní. Tedy $a$ je prvočíselné.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist. Sei $a$ ein Element von $M$ derart, dass $a$ irreduzibl und primal ist. Dann ist $a$ prim.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla. Låt $a$ vara ett element av $M$ sådant att $a$ är irreducibelt och primalt. Då är $a$ primt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), a \in M , \mathrm{Irreducible} (a), \mathrm{IsPrimal} (a)\vdash \mathrm{Prime} (a)$
Irreducible.primetheoremDefs.lean:150
Lean
theorem Irreducible.prime [DecompositionMonoid M] {a : M} (irr : Irreducible a) : Prime a :=
  irr.prime_of_isPrimal (DecompositionMonoid.primal a)
Dedukti
2 lines
def Irreducible__prime : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (_ : Proof (DecompositionMonoid M)) -> (a : Elem M) -> (irr : Proof (Irreducible a)) -> Proof (Prime a) :=
  M => x => h => a => irr => Irreducible__prime_of_isPrimal M a irr (DecompositionMonoid__primal M SemigroupWithZero__toSemigroup a).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero and $M$ is a decomposition monoid. Let $a$ be an irreducible element of $M$. Then $a$ is prime.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif et $M$ soit un monoïde de décompositions. Soit $a$ un élément de $M$ irréductible. Alors $a$ est premier.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou a $M$ je rozkladmonoid. Nechť $a$ je ireducibilní prvek $M$. Tedy $a$ je prvočíselné.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist und $M$ ein ZerlegungsMonoid ist. Sei $a$ ein irreduzibles Element von $M$. Dann ist $a$ prim.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla och $M$ är en uppdelningmonoid. Låt $a$ vara ett irreducibelt element av $M$. Då är $a$ primt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), \mathrm{DecompositionMonoid} (M), a \in M , \mathrm{Irreducible} (a)\vdash \mathrm{Prime} (a)$
Proof
5 lines
1.Let $a$ be an element of $M$.
2.Assume that $a$ is irreducible.
3.$x$ is a semigroup.SemigroupWithZero.toSemigroup
4.$a$ is primal.DecompositionMonoid.primal 3
5.$a$ is prime.Irreducible.prime_of_isPrimal 2, 4
Proof, French
5 lines
1.Soit $a$ un élément de $M$.
2.Supposons que $a$ est irréductible.
3.$x$ est un demi-groupe.SemigroupWithZero.toSemigroup
4.$a$ est primal.DecompositionMonoid.primal 3
5.$a$ est premier.Irreducible.prime_of_isPrimal 2, 4
Proof, Czech
5 lines
1.Nechť $a$ je prvek $M$.
2.Předpokládejme, že $a$ je ireducibilní.
3.$x$ je pologrupa.SemigroupWithZero.toSemigroup
4.$a$ je prvotní.DecompositionMonoid.primal 3
5.$a$ je prvočíselné.Irreducible.prime_of_isPrimal 2, 4
Proof, German
5 lines
1.Sei $a$ ein Element von $M$.
2.Nimm an, dass $a$ irreduzibl ist.
3.$x$ ist eine Halbgruppe.SemigroupWithZero.toSemigroup
4.$a$ ist primal.DecompositionMonoid.primal 3
5.$a$ ist prim.Irreducible.prime_of_isPrimal 2, 4
Proof, Swedish
5 lines
1.Låt $a$ vara ett element av $M$.
2.Anta att $a$ är irreducibelt.
3.$\mathrm{Semigroup}$ håller för $x$.SemigroupWithZero.toSemigroup
4.$a$ är primalt.DecompositionMonoid.primal 3
5.$a$ är primt.Irreducible.prime_of_isPrimal 2, 4
Prime.irreducibletheoremDefs.lean:159
Lean
protected theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
  ⟨hp.not_isUnit, fun a b ↦ by
    rintro rfl
    exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)⟩
Dedukti
2 lines
def Prime__irreducible : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (_ : Proof (IsCancelMulZero M)) -> (p : Elem M) -> (hp : Proof (Prime p)) -> Proof (Irreducible p) :=
  M => x => h => p => hp => Irreducible__mk (Prime__not_isUnit M p hp) (forallI M (a => forall M (b1 => if (Eqt M p (times a b1)) (or (IsUnit a) (IsUnit b1)))) (a => forallI M (b => if (Eqt M p (times a b)) (or (IsUnit a) (IsUnit b))) (b => ifI (Eqt M p (times a b)) (or (IsUnit a) (IsUnit b)) (h1 => Eq__ndrec (ifI (Prime (times a b)) (or (IsUnit a) (IsUnit b)) (hp1 => Or__imp (divide (times a b) b) (IsUnit a) (divide (times a b) a) (IsUnit b) (ifI (divide (times a b) b) (IsUnit a) (h2 => isUnit_of_dvd_one M a (iffEl (divide (times a b) (times 1 b)) (divide a 1) (mul_dvd_mul_iff_right M a 1 b (right_ne_zero_of_mul M a b (Prime__ne_zero M (times a b) hp1))) (dvd_mul_of_dvd_right M (times a b) b h2 1)))) (ifI (divide (times a b) a) (IsUnit b) (h3 => isUnit_of_dvd_one M b (iffEl (divide (times a b) (times a 1)) (divide b 1) (mul_dvd_mul_iff_left M a b 1 (left_ne_zero_of_mul M a b (Prime__ne_zero M (times a b) hp1))) (dvd_mul_of_dvd_left M (times a b) a h3 1)))) (Or__symm (divide (times a b) a) (divide (times a b) b) (Prime__dvd_or_dvd M (times a b) hp1 a b (dvd_rfl M (times a b)))))) (Eq__symm M p (times a b) h1) hp)))).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero and $M$ is cancellative. Let $p$ be a prime element of $M$. Then $p$ is irreducible.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif et $M$ soit cancellatif. Soit $p$ un élément de $M$ premier. Alors $p$ est irréductible.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou a $M$ je kancelativní. Nechť $p$ je prvočíselný prvek $M$. Tedy $p$ je ireducibilní.
German
Sei $M$ eine Menge derart, dass $M$ ein kommutatives Monoid mit Null ist und $M$ kürzbar ist. Sei $p$ ein primes Element von $M$. Dann ist $p$ irreduzibl.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla och $M$ är förkortningsbart. Låt $p$ vara ett primt element av $M$. Då är $p$ irreducibelt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), \mathrm{IsCancelMulZero} (M), p \in M , \mathrm{Prime} (p)\vdash \mathrm{Irreducible} (p)$
Proof
2 lines
1.Let $p$ be an element of $M$.
2.$\mathrm{forallI}$ applied to $M$, the function that maps $a$ to the proposition that for all elements $b_{1}$ of $M$, if $\EqtMACRoJ {p}{a \times b_{1}}$, then $a$ is a unit or $b_{1}$ is a unit and the function that maps $a$ to $\mathrm{forallI}$ applied to $M$, the function that maps $b$ to the proposition that if $\EqtMACRoJ {p}{a \times b}$, then $a$ is a unit or $b$ is a unit and the function that maps $b$ to $\mathrm{ifI}$ applied to $\EqtMACRoJ {p}{(a \times b)}$, the proposition that $a$ is a unit or $b$ is a unit and the function that maps $h_{1}$ to $\operatorname{ndrec}$ applied to $\mathrm{ifI}$ applied to the proposition that $a \times b$ is prime, the proposition that $a$ is a unit or $b$ is a unit and the function that maps $\mathrm{hp1}$ to $\operatorname{imp}$ applied to $\divides {(a \times b)}{b}$, the proposition that $a$ is a unit, $\divides {(a \times b)}{a}$, the proposition that $b$ is a unit, $\mathrm{ifI}$ applied to $\divides {(a \times b)}{b}$, the proposition that $a$ is a unit and the function that maps $h_{2}$ to $\mathrm{isUnit\_of\_dvd\_one}$ applied to $M$, $a$ and $\mathrm{iffEl}$ applied to $\divides {(a \times b)}{(1 \times b)}$, $\divides {a}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_right}$ applied to $M$, $a$, $1$, $b$ and $\mathrm{right\_ne\_zero\_of\_mul}$ applied to $M$, $a$, $b$ and $\mathrm{Prime\_\_ne\_zero}$ applied to $M$, $a \times b$ and $\mathrm{hp1}$ and $\mathrm{dvd\_mul\_of\_dvd\_right}$ applied to $M$, $a \times b$, $b$, $h_{2}$ and $1$, $\mathrm{ifI}$ applied to $\divides {(a \times b)}{a}$, the proposition that $b$ is a unit and the function that maps $h_{3}$ to $\mathrm{isUnit\_of\_dvd\_one}$ applied to $M$, $b$ and $\mathrm{iffEl}$ applied to $\divides {(a \times b)}{(a \times 1)}$, $\divides {b}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_left}$ applied to $M$, $a$, $b$, $1$ and $\mathrm{left\_ne\_zero\_of\_mul}$ applied to $M$, $a$, $b$ and $\mathrm{Prime\_\_ne\_zero}$ applied to $M$, $a \times b$ and $\mathrm{hp1}$ and $\mathrm{dvd\_mul\_of\_dvd\_left}$ applied to $M$, $a \times b$, $a$, $h_{3}$ and $1$ and $\operatorname{symm}$ applied to $\divides {(a \times b)}{a}$, $\divides {(a \times b)}{b}$ and $\mathrm{Prime\_\_dvd\_or\_dvd}$ applied to $M$, $a \times b$, $\mathrm{hp1}$, $a$, $b$ and $\mathrm{dvd\_rfl}$ applied to $M$ and $a \times b$, $\operatorname{symm}$ applied to $M$, $p$, $a \times b$ and $h_{1}$ and $\mathrm{hp}$ is irreducible.Irreducible.mk
Proof, French
2 lines
1.Soit $p$ un élément de $M$.
2.$\mathrm{forallI}$ appliqué à $M$, la fonction qui envoie $a$ à la proposition que pour tous les éléments $b_{1}$ de $M$, si $\EqtMACRoJ {p}{a \times b_{1}}$, alors $a$ est une unité ou $b_{1}$ est une unité et la fonction qui envoie $a$ à $\mathrm{forallI}$ appliqué à $M$, la fonction qui envoie $b$ à la proposition que si $\EqtMACRoJ {p}{a \times b}$, alors $a$ est une unité ou $b$ est une unité et la fonction qui envoie $b$ à $\mathrm{ifI}$ appliqué à $\EqtMACRoJ {p}{(a \times b)}$, la proposition que $a$ est une unité ou $b$ est une unité et la fonction qui envoie $h_{1}$ à $\operatorname{ndrec}$ appliqué à $\mathrm{ifI}$ appliqué à la proposition que $a \times b$ est premier, la proposition que $a$ est une unité ou $b$ est une unité et la fonction qui envoie $\mathrm{hp1}$ à $\operatorname{imp}$ appliqué à $\divides {(a \times b)}{b}$, la proposition que $a$ est une unité, $\divides {(a \times b)}{a}$, la proposition que $b$ est une unité, $\mathrm{ifI}$ appliqué à $\divides {(a \times b)}{b}$, la proposition que $a$ est une unité et la fonction qui envoie $h_{2}$ à $\mathrm{isUnit\_of\_dvd\_one}$ appliqué à $M$, $a$ et $\mathrm{iffEl}$ appliqué à $\divides {(a \times b)}{(1 \times b)}$, $\divides {a}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_right}$ appliqué à $M$, $a$, $1$, $b$ et $\mathrm{right\_ne\_zero\_of\_mul}$ appliqué à $M$, $a$, $b$ et $\mathrm{Prime\_\_ne\_zero}$ appliqué à $M$, $a \times b$ et $\mathrm{hp1}$ et $\mathrm{dvd\_mul\_of\_dvd\_right}$ appliqué à $M$, $a \times b$, $b$, $h_{2}$ et $1$, $\mathrm{ifI}$ appliqué à $\divides {(a \times b)}{a}$, la proposition que $b$ est une unité et la fonction qui envoie $h_{3}$ à $\mathrm{isUnit\_of\_dvd\_one}$ appliqué à $M$, $b$ et $\mathrm{iffEl}$ appliqué à $\divides {(a \times b)}{(a \times 1)}$, $\divides {b}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_left}$ appliqué à $M$, $a$, $b$, $1$ et $\mathrm{left\_ne\_zero\_of\_mul}$ appliqué à $M$, $a$, $b$ et $\mathrm{Prime\_\_ne\_zero}$ appliqué à $M$, $a \times b$ et $\mathrm{hp1}$ et $\mathrm{dvd\_mul\_of\_dvd\_left}$ appliqué à $M$, $a \times b$, $a$, $h_{3}$ et $1$ et $\operatorname{symm}$ appliqué à $\divides {(a \times b)}{a}$, $\divides {(a \times b)}{b}$ et $\mathrm{Prime\_\_dvd\_or\_dvd}$ appliqué à $M$, $a \times b$, $\mathrm{hp1}$, $a$, $b$ et $\mathrm{dvd\_rfl}$ appliqué à $M$ et $a \times b$, $\operatorname{symm}$ appliqué à $M$, $p$, $a \times b$ et $h_{1}$ et $\mathrm{hp}$ est irréductible.Irreducible.mk
Proof, Czech
2 lines
1.Nechť $p$ je prvek $M$.
2.$\mathrm{forallI}$ aplikovaný na $M$, funkci která zobrazuje $a$ na výrok že pro všechny prvky $b_{1}$ $M$, jestliže $\EqtMACRoJ {p}{a \times b_{1}}$, pak $a$ je jednotka nebo $b_{1}$ je jednotka a funkci která zobrazuje $a$ na $\mathrm{forallI}$ aplikovaný na $M$, funkci která zobrazuje $b$ na výrok že jestliže $\EqtMACRoJ {p}{a \times b}$, pak $a$ je jednotka nebo $b$ je jednotka a funkci která zobrazuje $b$ na $\mathrm{ifI}$ aplikovaný na $\EqtMACRoJ {p}{(a \times b)}$, výrok že $a$ je jednotka nebo $b$ je jednotka a funkci která zobrazuje $h_{1}$ na $\operatorname{ndrec}$ aplikovaný na $\mathrm{ifI}$ aplikovaný na výrok že $a \times b$ je prvočíselné, výrok že $a$ je jednotka nebo $b$ je jednotka a funkci která zobrazuje $\mathrm{hp1}$ na $\operatorname{imp}$ aplikovaný na $\divides {(a \times b)}{b}$, výrok že $a$ je jednotka, $\divides {(a \times b)}{a}$, výrok že $b$ je jednotka, $\mathrm{ifI}$ aplikovaný na $\divides {(a \times b)}{b}$, výrok že $a$ je jednotka a funkci která zobrazuje $h_{2}$ na $\mathrm{isUnit\_of\_dvd\_one}$ aplikovaný na $M$, $a$ a $\mathrm{iffEl}$ aplikovaný na $\divides {(a \times b)}{(1 \times b)}$, $\divides {a}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_right}$ aplikovaný na $M$, $a$, $1$, $b$ a $\mathrm{right\_ne\_zero\_of\_mul}$ aplikovaný na $M$, $a$, $b$ a $\mathrm{Prime\_\_ne\_zero}$ aplikovaný na $M$, $a \times b$ a $\mathrm{hp1}$ a $\mathrm{dvd\_mul\_of\_dvd\_right}$ aplikovaný na $M$, $a \times b$, $b$, $h_{2}$ a $1$, $\mathrm{ifI}$ aplikovaný na $\divides {(a \times b)}{a}$, výrok že $b$ je jednotka a funkci která zobrazuje $h_{3}$ na $\mathrm{isUnit\_of\_dvd\_one}$ aplikovaný na $M$, $b$ a $\mathrm{iffEl}$ aplikovaný na $\divides {(a \times b)}{(a \times 1)}$, $\divides {b}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_left}$ aplikovaný na $M$, $a$, $b$, $1$ a $\mathrm{left\_ne\_zero\_of\_mul}$ aplikovaný na $M$, $a$, $b$ a $\mathrm{Prime\_\_ne\_zero}$ aplikovaný na $M$, $a \times b$ a $\mathrm{hp1}$ a $\mathrm{dvd\_mul\_of\_dvd\_left}$ aplikovaný na $M$, $a \times b$, $a$, $h_{3}$ a $1$ a $\operatorname{symm}$ aplikovaný na $\divides {(a \times b)}{a}$, $\divides {(a \times b)}{b}$ a $\mathrm{Prime\_\_dvd\_or\_dvd}$ aplikovaný na $M$, $a \times b$, $\mathrm{hp1}$, $a$, $b$ a $\mathrm{dvd\_rfl}$ aplikovaný na $M$ a $a \times b$, $\operatorname{symm}$ aplikovaný na $M$, $p$, $a \times b$ a $h_{1}$ a $\mathrm{hp}$ je ireducibilní.Irreducible.mk
Proof, German
2 lines
1.Sei $p$ ein Element von $M$.
2.$\mathrm{forallI}$ angewandt auf $M$, die Funktion, die $a$ als der Satz, dass für alle Elemente $b_{1}$ von $M$, wenn $\EqtMACRoJ {p}{a \times b_{1}}$, dann $a$ eine Einheit ist oder $b_{1}$ eine Einheit ist, abbildet, und die Funktion, die $a$ als $\mathrm{forallI}$ angewandt auf $M$, die Funktion, die $b$ als der Satz, dass wenn $\EqtMACRoJ {p}{a \times b}$, dann $a$ eine Einheit ist oder $b$ eine Einheit ist, abbildet, und die Funktion, die $b$ als $\mathrm{ifI}$ angewandt auf $\EqtMACRoJ {p}{(a \times b)}$, den Satz, dass $a$ eine Einheit ist oder $b$ eine Einheit ist, und die Funktion, die $h_{1}$ als $\operatorname{ndrec}$ angewandt auf $\mathrm{ifI}$ angewandt auf den Satz, dass $a \times b$ prim ist, den Satz, dass $a$ eine Einheit ist oder $b$ eine Einheit ist, und die Funktion, die $\mathrm{hp1}$ als $\operatorname{imp}$ angewandt auf $\divides {(a \times b)}{b}$, den Satz, dass $a$ eine Einheit ist, $\divides {(a \times b)}{a}$, den Satz, dass $b$ eine Einheit ist, $\mathrm{ifI}$ angewandt auf $\divides {(a \times b)}{b}$, den Satz, dass $a$ eine Einheit ist, und die Funktion, die $h_{2}$ als $\mathrm{isUnit\_of\_dvd\_one}$ angewandt auf $M$, $a$ und $\mathrm{iffEl}$ angewandt auf $\divides {(a \times b)}{(1 \times b)}$, $\divides {a}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_right}$ angewandt auf $M$, $a$, $1$, $b$ und $\mathrm{right\_ne\_zero\_of\_mul}$ angewandt auf $M$, $a$, $b$ und $\mathrm{Prime\_\_ne\_zero}$ angewandt auf $M$, $a \times b$ und $\mathrm{hp1}$ und $\mathrm{dvd\_mul\_of\_dvd\_right}$ angewandt auf $M$, $a \times b$, $b$, $h_{2}$ und $1$ abbildet, $\mathrm{ifI}$ angewandt auf $\divides {(a \times b)}{a}$, den Satz, dass $b$ eine Einheit ist, und die Funktion, die $h_{3}$ als $\mathrm{isUnit\_of\_dvd\_one}$ angewandt auf $M$, $b$ und $\mathrm{iffEl}$ angewandt auf $\divides {(a \times b)}{(a \times 1)}$, $\divides {b}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_left}$ angewandt auf $M$, $a$, $b$, $1$ und $\mathrm{left\_ne\_zero\_of\_mul}$ angewandt auf $M$, $a$, $b$ und $\mathrm{Prime\_\_ne\_zero}$ angewandt auf $M$, $a \times b$ und $\mathrm{hp1}$ und $\mathrm{dvd\_mul\_of\_dvd\_left}$ angewandt auf $M$, $a \times b$, $a$, $h_{3}$ und $1$ abbildet, und $\operatorname{symm}$ angewandt auf $\divides {(a \times b)}{a}$, $\divides {(a \times b)}{b}$ und $\mathrm{Prime\_\_dvd\_or\_dvd}$ angewandt auf $M$, $a \times b$, $\mathrm{hp1}$, $a$, $b$ und $\mathrm{dvd\_rfl}$ angewandt auf $M$ und $a \times b$ abbildet, $\operatorname{symm}$ angewandt auf $M$, $p$, $a \times b$ und $h_{1}$ und $\mathrm{hp}$ abbildet, abbildet, abbildet, ist irreduzibl.Irreducible.mk
Proof, Swedish
2 lines
1.Låt $p$ vara ett element av $M$.
2.$\mathrm{forallI}$ applicerat på $M$, funktionen som avbildar $a$ som påståendet att för alla element $b_{1}$ av $M$, om $\EqtMACRoJ {p}{a \times b_{1}}$, så är $a$ en enhet eller $b_{1}$ är en enhet och funktionen som avbildar $a$ som $\mathrm{forallI}$ applicerat på $M$, funktionen som avbildar $b$ som påståendet att om $\EqtMACRoJ {p}{a \times b}$, så är $a$ en enhet eller $b$ är en enhet och funktionen som avbildar $b$ som $\mathrm{ifI}$ applicerat på $\EqtMACRoJ {p}{(a \times b)}$, påståendet att $a$ är en enhet eller $b$ är en enhet och funktionen som avbildar $h_{1}$ som $\operatorname{ndrec}$ applicerat på $\mathrm{ifI}$ applicerat på påståendet att $a \times b$ är primt, påståendet att $a$ är en enhet eller $b$ är en enhet och funktionen som avbildar $\mathrm{hp1}$ som $\operatorname{imp}$ applicerat på $\divides {(a \times b)}{b}$, påståendet att $a$ är en enhet, $\divides {(a \times b)}{a}$, påståendet att $b$ är en enhet, $\mathrm{ifI}$ applicerat på $\divides {(a \times b)}{b}$, påståendet att $a$ är en enhet och funktionen som avbildar $h_{2}$ som $\mathrm{isUnit\_of\_dvd\_one}$ applicerat på $M$, $a$ och $\mathrm{iffEl}$ applicerat på $\divides {(a \times b)}{(1 \times b)}$, $\divides {a}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_right}$ applicerat på $M$, $a$, $1$, $b$ och $\mathrm{right\_ne\_zero\_of\_mul}$ applicerat på $M$, $a$, $b$ och $\mathrm{Prime\_\_ne\_zero}$ applicerat på $M$, $a \times b$ och $\mathrm{hp1}$ och $\mathrm{dvd\_mul\_of\_dvd\_right}$ applicerat på $M$, $a \times b$, $b$, $h_{2}$ och $1$, $\mathrm{ifI}$ applicerat på $\divides {(a \times b)}{a}$, påståendet att $b$ är en enhet och funktionen som avbildar $h_{3}$ som $\mathrm{isUnit\_of\_dvd\_one}$ applicerat på $M$, $b$ och $\mathrm{iffEl}$ applicerat på $\divides {(a \times b)}{(a \times 1)}$, $\divides {b}{1}$, $\mathrm{mul\_dvd\_mul\_iff\_left}$ applicerat på $M$, $a$, $b$, $1$ och $\mathrm{left\_ne\_zero\_of\_mul}$ applicerat på $M$, $a$, $b$ och $\mathrm{Prime\_\_ne\_zero}$ applicerat på $M$, $a \times b$ och $\mathrm{hp1}$ och $\mathrm{dvd\_mul\_of\_dvd\_left}$ applicerat på $M$, $a \times b$, $a$, $h_{3}$ och $1$ och $\operatorname{symm}$ applicerat på $\divides {(a \times b)}{a}$, $\divides {(a \times b)}{b}$ och $\mathrm{Prime\_\_dvd\_or\_dvd}$ applicerat på $M$, $a \times b$, $\mathrm{hp1}$, $a$, $b$ och $\mathrm{dvd\_rfl}$ applicerat på $M$ och $a \times b$, $\operatorname{symm}$ applicerat på $M$, $p$, $a \times b$ och $h_{1}$ och $\mathrm{hp}$ är irreducibelt.Irreducible.mk
irreducible_iff_primetheoremDefs.lean:168
Lean
theorem irreducible_iff_prime [DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a :=
  ⟨Irreducible.prime, Prime.irreducible⟩
Dedukti
2 lines
def irreducible_iff_prime : (M : Set) -> (_ : Proof (CommMonoidWithZero M)) -> (_ : Proof (IsCancelMulZero M)) -> (_ : Proof (DecompositionMonoid M)) -> (a : Elem M) -> Proof (iff (Irreducible a) (Prime a)) :=
  M => x => h => h1 => a => iffI (Irreducible a) (Prime a) (Irreducible__prime M a) (Prime__irreducible M a).
English
Let $M$ be a set such that $M$ is a commutative monoid with zero, $M$ is cancellative and $M$ is a decomposition monoid. Let $a$ be an element of $M$. Then $a$ is irreducible, if and only if $a$ is prime.
French
Soit $M$ un ensemble tel que $M$ soit un monoïde avec du zéro commutatif, $M$ soit cancellatif et $M$ soit un monoïde de décompositions. Soit $a$ un élément de $M$. Alors $a$ est irréductible si et seulement si $a$ est premier.
Czech
Nechť $M$ je množina taková, že $M$ je komutativní monoid s nulou, $M$ je kancelativní a $M$ je rozkladmonoid. Nechť $a$ je prvek $M$. Tedy $a$ je ireducibilní, právě tehdy, když $a$ je prvočíselné.
German
Sei $M$ eine Menge derart, dass ist $M$ ein kommutatives Monoid mit Null, $M$ kürzbar ist und $M$ ein ZerlegungsMonoid ist. Sei $a$ ein Element von $M$. Dann ist $a$ irreduzibl, genau dann, wenn $a$ prim ist.
Swedish
Låt $M$ vara en mängd sådan att $M$ är en kommutativ monoid med nolla, $M$ är förkortningsbart och $M$ är en uppdelningmonoid. Låt $a$ vara ett element av $M$. Då är $a$ irreducibelt, om och endast om $a$ är primt.
Formula
$M \in \mathrm{Set} , \mathrm{CommMonoidWithZero} (M), \mathrm{IsCancelMulZero} (M), \mathrm{DecompositionMonoid} (M), a \in M \vdash \mathrm{Irreducible} (a)\leftrightarrow \mathrm{Prime} (a)$
Proof
4 lines
1.Let $a$ be an element of $M$.
2.$a$ is prime.Irreducible.prime
3.$a$ is irreducible.Prime.irreducible
4.$a$ is irreducible, if and only if $a$ is prime.iffI 2, 3
Proof, French
4 lines
1.Soit $a$ un élément de $M$.
2.$a$ est premier.Irreducible.prime
3.$a$ est irréductible.Prime.irreducible
4.$a$ est irréductible si et seulement si $a$ est premier.iffI 2, 3
Proof, Czech
4 lines
1.Nechť $a$ je prvek $M$.
2.$a$ je prvočíselné.Irreducible.prime
3.$a$ je ireducibilní.Prime.irreducible
4.$a$ je ireducibilní, právě tehdy, když $a$ je prvočíselné.iffI 2, 3
Proof, German
4 lines
1.Sei $a$ ein Element von $M$.
2.$a$ ist prim.Irreducible.prime
3.$a$ ist irreduzibl.Prime.irreducible
4.$a$ ist irreduzibl, genau dann, wenn $a$ prim ist.iffI 2, 3
Proof, Swedish
4 lines
1.Låt $a$ vara ett element av $M$.
2.$a$ är primt.Irreducible.prime
3.$a$ är irreducibelt.Prime.irreducible
4.$a$ är irreducibelt, om och endast om $a$ är primt.iffI 2, 3