Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325): Difference between revisions

@@ Property / describes a project that uses @@
+Lifting
@@ Property / describes a project that uses: Lifting / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Transfer
@@ Property / describes a project that uses: Transfer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Poly/ML
@@ Property / describes a project that uses: Poly/ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cayley-Hamilton
@@ Property / describes a project that uses: Cayley-Hamilton / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gauss-Jordan
@@ Property / describes a project that uses: Gauss-Jordan / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+QR Decomposition
@@ Property / describes a project that uses: QR Decomposition / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jordan Normal Forms
@@ Property / describes a project that uses: Jordan Normal Forms / 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/s00165-016-0383-1
+Normal rank
@@ Property / OpenAlex ID @@
+W2471798638
@@ Property / OpenAlex ID: W2471798638 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization and Execution of Linear Algebra: From Theorems to Algorithms
+Normal rank
@@ Property / cites work @@
+Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
+Normal rank
@@ Property / cites work @@
+Q4827633
@@ Property / cites work: Q4827633 / rank @@
+Normal rank
@@ Property / cites work @@
+Fast parallel matrix and GCD computations
@@ Property / cites work: Fast parallel matrix and GCD computations / rank @@
+Normal rank
@@ Property / cites work @@
+Q4831098
@@ Property / cites work: Q4831098 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalized linear algebra over Elementary Divisor Rings in Coq
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+A Refinement-Based Approach to Computational Algebra in Coq
+Normal rank
@@ Property / cites work @@
+Q4513600
@@ Property / cites work: Q4513600 / rank @@
+Normal rank
@@ Property / cites work @@
+Commutative algebra in the Mizar system
@@ Property / cites work: Commutative algebra in the Mizar system / rank @@
+Normal rank
@@ Property / cites work @@
+The HOL Light theory of Euclidean space
@@ Property / cites work: The HOL Light theory of Euclidean space / rank @@
+Normal rank
@@ Property / cites work @@
+Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Q4771385
@@ Property / cites work: Q4771385 / rank @@
+Normal rank
@@ Property / cites work @@
+Animating the Formalised Semantics of a Java-Like Language
+Normal rank
@@ Property / cites work @@
+Q4517538
@@ Property / cites work: Q4517538 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3224016
@@ Property / cites work: Q3224016 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5668937
@@ Property / cites work: Q5668937 / rank @@
+Normal rank
@@ Property / cites work @@
+Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
+Normal rank
@@ Property / cites work @@
+Computation of approximate polynomial GCDs and an extension
+Normal rank
@@ Property / cites work @@
+Q5195247
@@ Property / cites work: Q5195247 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5847989
@@ Property / cites work: Q5847989 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5743906
@@ Property / cites work: Q5743906 / rank @@
+Normal rank