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.0.tar.gz
sha256=0df32351777137cac4ee4380de2e93358298738d81842008ba32fe748d8acfa5

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-04-26 logpath:FinMatrix

Published: 26 Apr 2024

Dependencies (1)

  1. coq >= "8.18.0"

Dev Dependencies

None

Used by

None

Conflicts

None