Finite Field
30-sec diagnosis
Back to NPA

Module

Mathlib.Vector.Basic

npa-mathlib

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Theorems

12

Definitions

4

Inductive types

1

Axioms

0

Declarations

vec_zero

Vec

definition

vec_add

forall (u : Vec), forall (v : Vec), Vec

definition

vec_neg

forall (v : Vec), Vec

definition

vec_sub

forall (u : Vec), forall (v : Vec), Vec

definition

vec_add_assoc

forall (u : Vec), forall (v : Vec), forall (w : Vec), @Eq.{1} Vec (vec_add (vec_add u v) w) (vec_add u (vec_add v w))

theorem

vec_add_comm

forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_add u v) (vec_add v u)

theorem

vec_zero_add

forall (v : Vec), @Eq.{1} Vec (vec_add vec_zero v) v

theorem

vec_add_zero

forall (v : Vec), @Eq.{1} Vec (vec_add v vec_zero) v

theorem

vec_neg_add_cancel

forall (v : Vec), @Eq.{1} Vec (vec_add (vec_neg v) v) vec_zero

theorem

vec_add_neg_cancel

forall (v : Vec), @Eq.{1} Vec (vec_add v (vec_neg v)) vec_zero

theorem

vec_sub_def

forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_sub u v) (vec_add u (vec_neg v))

theorem

vec_sub_eq_add_neg

forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_sub u v) (vec_add u (vec_neg v))

theorem

vec_sub_self

forall (v : Vec), @Eq.{1} Vec (vec_sub v v) vec_zero

theorem

vec_sub_zero

forall (v : Vec), @Eq.{1} Vec (vec_sub v vec_zero) v

theorem

vec_add_left_cancel

forall (u : Vec), forall (v : Vec), forall (w : Vec), forall (h : @Eq.{1} Vec (vec_add u v) (vec_add u w)), @Eq.{1} Vec v w

theorem

sub_sub_sub_cancel

forall (u : Vec), forall (v : Vec), forall (w : Vec), @Eq.{1} Vec (vec_sub (vec_sub u w) (vec_sub v w)) (vec_sub u v)

theorem

Vec

Type

inductive

Hashes

source
sha256:19db7e04cd08724e4f8e393786e86caac000a62a408b5ac25b9024e741f262a0
certificateFile
sha256:5b5f20f683c498127c652a98d56b2838d098c5b3aa3adaa54dd4675748fdfbab
export
sha256:3ba8f7b514c7f041a1ac86bf1800a21186255bac9ce31e2fea0b7d9c91d4c938
axiomReport
sha256:55932adb6d068a32ac76b43afee2b808d61b89bb36b85b1805fe77d82a1028b3
certificate
sha256:fb89a6e1e47b9622b5e77b7dd8d12acb04073bba76e1ef7cffe76130f981f423

Source

import Std.Logic.Eq

inductive Vec :
  Type where
| unit : Vec

def vec_zero :
  Vec :=
  Vec.unit

def vec_add :
  forall (u : Vec), forall (v : Vec), Vec :=
  fun u => fun v => Vec.unit

def vec_neg :
  forall (v : Vec), Vec :=
  fun v => Vec.unit

def vec_sub :
  forall (u : Vec), forall (v : Vec), Vec :=
  fun u => fun v => vec_add u (vec_neg v)

theorem vec_add_assoc :
  forall (u : Vec), forall (v : Vec), forall (w : Vec), @Eq.{1} Vec (vec_add (vec_add u v) w) (vec_add u (vec_add v w)) :=
  fun u => fun v => fun w => @Eq.refl.{1} Vec (vec_add (vec_add u v) w)

theorem vec_add_comm :
  forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_add u v) (vec_add v u) :=
  fun u => fun v => @Eq.refl.{1} Vec (vec_add u v)

theorem vec_zero_add :
  forall (v : Vec), @Eq.{1} Vec (vec_add vec_zero v) v :=
  fun v => @Vec.rec.{0} (fun (x : Vec) => @Eq.{1} Vec Vec.unit x) (@Eq.refl.{1} Vec Vec.unit) v

theorem vec_add_zero :
  forall (v : Vec), @Eq.{1} Vec (vec_add v vec_zero) v :=
  fun v => @Vec.rec.{0} (fun (x : Vec) => @Eq.{1} Vec Vec.unit x) (@Eq.refl.{1} Vec Vec.unit) v

theorem vec_neg_add_cancel :
  forall (v : Vec), @Eq.{1} Vec (vec_add (vec_neg v) v) vec_zero :=
  fun v => @Eq.refl.{1} Vec (vec_add (vec_neg v) v)

theorem vec_add_neg_cancel :
  forall (v : Vec), @Eq.{1} Vec (vec_add v (vec_neg v)) vec_zero :=
  fun v => @Eq.refl.{1} Vec (vec_add v (vec_neg v))

theorem vec_sub_def :
  forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_sub u v) (vec_add u (vec_neg v)) :=
  fun u => fun v => @Eq.refl.{1} Vec (vec_sub u v)

theorem vec_sub_eq_add_neg :
  forall (u : Vec), forall (v : Vec), @Eq.{1} Vec (vec_sub u v) (vec_add u (vec_neg v)) :=
  fun u => fun v => @Eq.refl.{1} Vec (vec_sub u v)

theorem vec_sub_self :
  forall (v : Vec), @Eq.{1} Vec (vec_sub v v) vec_zero :=
  fun v => @Eq.refl.{1} Vec (vec_sub v v)

theorem vec_sub_zero :
  forall (v : Vec), @Eq.{1} Vec (vec_sub v vec_zero) v :=
  fun v => @Vec.rec.{0} (fun (x : Vec) => @Eq.{1} Vec Vec.unit x) (@Eq.refl.{1} Vec Vec.unit) v

theorem vec_add_left_cancel :
  forall (u : Vec), forall (v : Vec), forall (w : Vec), forall (h : @Eq.{1} Vec (vec_add u v) (vec_add u w)), @Eq.{1} Vec v w :=
  fun u => fun v => fun w => fun h => @Vec.rec.{0} (fun (x : Vec) => @Eq.{1} Vec x w) (@Vec.rec.{0} (fun (y : Vec) => @Eq.{1} Vec Vec.unit y) (@Eq.refl.{1} Vec Vec.unit) w) v

theorem sub_sub_sub_cancel :
  forall (u : Vec), forall (v : Vec), forall (w : Vec), @Eq.{1} Vec (vec_sub (vec_sub u w) (vec_sub v w)) (vec_sub u v) :=
  fun u => fun v => fun w => @Eq.refl.{1} Vec (vec_sub (vec_sub u w) (vec_sub v w))