package coq-finmatrix

  1. Overview
  2. No Docs
Matrix by fin (finite set over nat) in Coq

Install

Dune Dependency

zhengpushi.github.io Edit opam file Versions (2)

Authors

  1. Z
    ZhengPu Shi

Maintainers

  1. Z
    zhengpushi@nuaa.edu.cn

Sources

v1.0.2.tar.gz
sha256=8f968758bfe470a696aa02feafe0ab19eda9e75ccd66f8c7f22f675974bd5d78

Description

FinMatrix is a formal matrix library in Coq, which we started from finite sets (over natural numbers), vecotr based on finite sets, and matrices based on vectors. This implementation differs from the CoqMatrix project(https://github.com/zhengpushi/CoqMatrix), which have various models.

We have formalized many algebraic and geometric vector or matrix theories, especially including two inversion matrix algorithms: minvGE (inversion based on Gauss Elimination), minvAM (inversion based on Adjoint Matrix).

Tags

keyword:matrices category:Mathematics/Algebra date:2024-06-11 logpath:FinMatrix

Published: 11 Jun 2024

Dependencies (1)

  1. coq >= "8.18.0"

Dev Dependencies

None

Used by

None

Conflicts

None