Top100MathematicalTheoremsInCoq - coq/coq GitHub Wiki

Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.

See: UserContributions/Nijmegen/QArithSternBrocot/sqrt2.v

~exists n, exists p, n ^2 = 2* p^2 /\ n <> 0

See: SquareRootTwo

Lemma FTA : forall f : CCX, nonConst _ f -> {z : CC | f ! z [=] Zero}.

Lemma FTA_a_la_Henk : forall f : CCX, {x : CC | {y : CC | AbsCC (f ! x[-]f ! y) [>]Zero}} -> {z : CC | f ! z [=] Zero}.

See: UserContributions/Nijmegen/CoRN/fta/FTA.v

Theorem Q_is_denumerable: is_denumerable Q.

where

Definition is_denumerable A := same_cardinality A nat.
Definition same_cardinality (A B:Set):= {f:A->B & { g:B->A |
  (forall b,(compose _ _ _ f g) b= (identity B) b) /\
   forall a,(compose _ _ _ g f) a = (identity A) a}}.

See: UserContributions/Nijmegen/QArithSternBrocot/Q_denumerable.v

Theorem Pythagore : forall A B C : PO, orthogonal (vec A B) (vec A C) <-> Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.

See: UserContributions/Sophia-Antipolis/geometry

forall T : System, Included Formula NN T -> RepresentsInSelf T -> DecidableSet Formula T -> { f : Formula | (Sentence f) /\ ({SysPrf T f} + {SysPrf T (notH f)} -> Inconsistent LNN T)}

See: UserContributions/Berkeley/Godel

~(EX l:(list Prime) | (p:Prime)(In p l))

See: NotFinitePrimes

Theorem Euler_Poincare_criterion: forall m:fmap, inv_qhmap m -> (plf m <-> ec m / 2 = nc m).

See: UserContributions/Strasbourg/EulerFormula

Lemma FTC1 : forall (J : interval) (F : PartFunct IR) (contF : Continuous J F) (x0 : IR) (Hx0 : J x0) (pJ : proper J), Derivative J pJ (([-S-]contF) x0 Hx0) F

Lemma FTC2 : forall (J : interval) (F : PartFunct IR) (contF : Continuous J F) (x0 : IR) (Hx0 : J x0) (pJ : proper J) (G0 : PartFunct IR), Derivative J pJ G0 F -> {c : IR | Feq J (([-S-]contF) x0 Hx0{-}G0) [-C-]c}

Lemma Barrow : forall (J : interval) (F : PartFunct IR), Continuous J F -> forall (pJ : proper J) (G0 : PartFunct IR) (derG0 : Derivative J pJ G0 F) (a b : IR) (H : Continuous_I (Min_leEq_Max a b) F) (Ha : J a) (Hb : J b), let Ha' := Derivative_imp_inc J pJ G0 F derG0 a Ha in let Hb' := Derivative_imp_inc J pJ G0 F derG0 b Hb in Integral H[=]G0 b Hb'[-]G0 a Ha'

See: UserContributions/Nijmegen/CoRN

See: UserContributions/Sophia-Antipolis

See: UserContributions/Nijmegen/CoRN

forall n, 0 <= n -> (forall p, prime p -> Zis_mod p 3 4 -> Zeven (Zdiv_exp p n)) -> sum_of_two_square n

See: UserContributions/Sophia-Antipolis/SumOfTwoSquare

Lemma pytha_thm1 : forall a b c : Z, (is_pytha a b c) -> (pytha_set a b c).

Lemma pytha_thm2 : forall a b c : Z, (pytha_set a b c) -> (is_pytha a b c).

See: UserContributions/CNAM/Fermat4 (File Pythagorean.v) by D. Delahaye and M. Mayero |

forall A B:Ensemble U, A <=_card B -> B <=_card A -> A =_card B.

See: UserContributions/Rocq/SCHROEDER

See: UserContributions/Nijmegen/CoRN

See: UserContributions/Sophia-Antipolis/

forall A B C A1 B1 C1 O A2 B2 C2 O2:point, forall r r2:R, X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0-> middle A B C1 -> middle B C A1 -> middle C A B1 -> distance2 O A1 = distance2 O B1 -> distance2 O A1 = distance2 O C1 -> collinear A B C2 -> orthogonal A B O2 C2 -> collinear B C A2 -> orthogonal B C O2 A2 -> collinear A C B2 -> orthogonal A C O2 B2 -> distance2 O2 A2 = distance2 O2 B2 -> distance2 O2 A2 = distance2 O2 C2 -> r^2 = distance2 O A1 -> r2^2 = distance2 O2 A2 -> distance2 O O2 = (r + r2)^2 \/ distance2 O O2 = (r - r2)^2 \/ collinear A B C.

See: http://www-sop.inria.fr/marelle/CertiGeo/feuerbach.html

See: Georges Gonthier http://research.microsoft.com/~gonthier/

Lemma Taylor : forall (I : interval) (pI : proper I) (F : PartFunct IR) (n : nat) (f : forall i : nat, i < S n -> PartFunct IR) (derF : forall (i : nat) (Hi : i < S n), Derivative_n i I pI F (f i Hi)) (F' : PartFunct IR), Derivative_n (S n) I pI F F' -> forall (a b : IR) (Ha : I a), I b -> forall e : IR, Zero[<]e -> forall Hb' : Dom F b, {c : IR | Compact (Min_leEq_Max a b) c | forall Hc : Dom (F'{*}[-C-](One[/]nring (fac n)[//]nring_fac_ap_zero IR n){*} ([-C-]b{-}FId){^}n) c, AbsIR (F b Hb'[-] Taylor_Seq I pI F n f derF a Ha b (Taylor_aux I pI F n f derF a b Ha)[-] (F'{*}[-C-](One[/]nring (fac n)[//]nring_fac_ap_zero IR n){*} ([-C-]b{-}FId){^}n) c Hc[*](b[-]a))[<=]e}

See: UserContributions/Nijmegen/CoRN

(a + b) ^ n = \sum_(i < n.+1) (bin n i * (a ^ (n - i) * b ^ i))

See: http://coqfinitgroup.gforge.inria.fr/binomial.html#exp_pascal

Every square matrix is a root of its characteristic polynomial : forall A, (Zpoly (char_poly A)).[A] = 0

See: Math Components Project : http://coqfinitgroup.gforge.inria.fr/charpoly.html#Cayley_Hamilton

forall p, prime p -> Zis_mod (Zfact (p - 1)) (- 1) p

See: UserContributions/Sophia-Antipolis/

forall p, 1 < p -> (prime p <-> p % (fact (p.-1)).+1)

See: http://coqfinitgroup.gforge.inria.fr/binomial.html#wilson

See: ??

forall A B C D M O:point, samedistance O A O B -> samedistance O A O C -> samedistance O A O D -> collinear A B M -> collinear C D M -> (distance M A)*(distance M B)=(distance M C)*(distance M D) \/ parallel A B C D.

See: to appear next...

See: StandardLibrary/Coq.ZArith.Znumtheory

forall m n, m > 0 -> {a | a < m & m %| gcdn m n + a * n}

forall m n, n > 0 -> {a | a < n & n %| gcdn m n + a * m}

See: http://coqfinitgroup.gforge.inria.fr/div.html#bezoutl

Theorem herron_qin : forall A B C, S A B C * S A B C = 1 / (2*2*2*2) * (Py A B A * Py A C A - Py B A C * Py B A C).

See: UserContributions/Rocq/AreaMethod/

Theorem Ceva : forall A B C D E F G P : Point, inter_ll D B C A P -> inter_ll E A C B P -> inter_ll F A B C P -> F <> B -> D <> C -> E <> A -> parallel A F F B -> parallel B D D C -> parallel C E E A -> (A** F / F ** B * (B ** D / D** C) * (C ** E / E** A) = 1.

See: UserContributions/Rocq/AreaMethod

See: UserContributions/Sophia-Antipolis UserContributions/Rocq/AreaMethod

Lemma power_series_conv : forall c : IR, AbsIR c[<]One -> convergent (power_series c)

Lemma power_series_sum : forall c : IR, AbsIR c[<]One -> forall (H : Dom (f_rcpcl' IR) (One[-]c)) (Hc0 : convergent (power_series c)), series_sum (power_series c) Hc0[=](One[/]One[-]c[//]H)

See: UserContributions/Nijmegen/CoRN

See: StandardLibrary/Coq.ZArith.Znumtheory

forall (gT : finGroupType) (G H : {group gT}), H :<=: G -> (#|H| * #|G : H|)%N = #|G|

See: http://coqfinitgroup.gforge.inria.fr/groups.html#LaGrange

Lemma Sylow_exists: forall (p : nat) (gT : finGroupType) (G : {group gT}), {P : {group gT} | p.-Sylow(G) P}

Lemma Sylow_subj: forall (p : nat) (gT : finGroupType) (G P Q : {group gT}), p.-Sylow(G) P -> Q :<=: G -> p.-group Q -> exists2 x : gT, x \in G & Q :<=: P :^ x

Lemma card_Syl_dvd : forall (p : nat) (gT : finGroupType) (G : {group gT}), #|'Syl_p(G)| %| #|G|

Lemma card_Syl_mod : forall (p : nat) (gT : finGroupType) (G : {group gT}), prime p -> #|'Syl_p(G)| %% p = 1

See: http://coqfinitgroup.gforge.inria.fr/sylow.html

forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

See: StandardLibrary

Lemma Law_of_the_Mean : forall (I : interval) (pI : proper I) (F F' : PartFunct IR), Derivative I pI F F' -> forall a b : IR, I a -> I b -> forall e : IR, Zero[<]e -> {x : IR | Compact (Min_leEq_Max a b) x | forall (Ha : Dom F a) (Hb : Dom F b) (Hx : Dom F' x), AbsIR (F b Hb[-]F a Ha[-]F' x Hx[*](b[-]a))[<=]e} Lemma Law_of_the_Mean_ineq : forall (I : interval) (pI : proper I) (F F' : PartFunct IR), Derivative I pI F F' -> forall a b : IR, I a -> I b -> forall c : IR, (forall x : IR, Compact (Min_leEq_Max a b) x -> forall Hx : Dom F' x, AbsIR (F' x Hx)[<=]c) -> forall (Ha : Dom F a) (Hb : Dom F b), F b Hb[-]F a Ha[<=]c[*]AbsIR (b[-]a)

See: UserContributions/Nijmegen/CoRN

Lemma Civt_op : forall f : CSetoid_un_op IR, contin f -> (forall a b : IR, a[<]b -> {c : IR | a[<=]c /\ c[<=]b | f c[#]Zero}) -> forall a b : IR, a[<]b -> f a[<=]Zero -> Zero[<=]f b -> {z : IR | a[<=]z /\ z[<=]b /\ f z[=]Zero}

See: UserContributions/Nijmegen/CoRN

See: UserContributions/Eindhoven/POCKLINGTON

Theorem Desargues : forall A B C X A' B' C' : Point, A' <>C' -> A' <> B' -> on_line A' X A -> on_inter_line_parallel B' A' X B A B -> on_inter_line_parallel C' A' X C A C -> parallel B C B' C'.

See: UserContributions/Rocq/AreaMethod UserContributions/Sophia-Antipolis/geometry

See: StandardLibrary

See: UserContributions/Sophia-Antipolis/

See: extension of UserContributions/Sophia-Antipolis/geometry/

forall (R : comRingType) (n : nat) (A : matrix R n n), A *m \adj A = \Z (\det A)

See: Math Components Project : http://coqfinitgroup.gforge.inria.fr/matrix.html#mulmx_adjr

forall n : nat, 2 <= n -> exists p : nat, prime p /\ n < p /\ p < 2 * n

See: UserContributions/Sophia-Antipolis/Bertrand

• The theorems regarding angles or triangles are proved in one of the two UserContributions/Sophia-Antipolis/geometry or UserContributions/Sophia-Antipolis/Angles (please specify if you know which contrib package contains them).
• The Ranks are taken from the original list of Top100MathematicalTheorems.
• See Also http://www.cs.ru.nl/~freek/100/