vec_add_left_cancel

Mathlib.Vector.Basic

Packages

Module

Theorems

750

Declarations

1016

Untrusted sidecar

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

Statement

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

Proof term

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

Constants

Mathlib.Vector.Basic.Vec

Interface hash: sha256:bc9e713ccaaae78bf5ef428fe3455d47b8f8432e58b79a82bf806866b713e287

Mathlib.Vector.Basic.vec_add

Interface hash: sha256:24f3c880ceca68e123a5fd883a7f48e39bd3b88832ec2f579c0879e2532bad2e

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015