A mechanized proof of the basic perturbation lemma (Q928666): Difference between revisions

@@ Property / author @@
-Julio Jesús Rubio García
@@ Property / author: Julio Jesús Rubio García / rank @@
-Normal rank
@@ Property / author @@
+Julio Jesús Rubio García
@@ Property / author: Julio Jesús Rubio García / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Kenzo
@@ Property / describes a project that uses: Kenzo / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-007-9094-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2027737519
@@ Property / OpenAlex ID: W2027737519 / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+Interpretation of Locales in Isabelle: Theories and Proof Contexts
+Normal rank
@@ Property / cites work @@
+A Fixed Point Approach to Homological Perturbation Theory
+Normal rank
@@ Property / cites work @@
+Q2766799
@@ Property / cites work: Q2766799 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435458
@@ Property / cites work: Q4435458 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+A logical approach to abstract algebra
@@ Property / cites work: A logical approach to abstract algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Constructive Homological Algebra in Type Theory
+Normal rank
@@ Property / cites work @@
+On the chain-complex of a fibration
@@ Property / cites work: On the chain-complex of a fibration / rank @@
+Normal rank
@@ Property / cites work @@
+Q4693118
@@ Property / cites work: Q4693118 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3783260
@@ Property / cites work: Q3783260 / rank @@
+Normal rank
@@ Property / cites work @@
+A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
+Normal rank
@@ Property / cites work @@
+On constructive mathematics
@@ Property / cites work: On constructive mathematics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247084
@@ Property / cites work: Q4247084 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q3972529
@@ Property / cites work: Q3972529 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive algebraic topology
@@ Property / cites work: Constructive algebraic topology / rank @@
+Normal rank
@@ Property / cites work @@
+Q4003339
@@ Property / cites work: Q4003339 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume I
+Normal rank