add_left_cancel

Mathlib.Algebra.Ring

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 (a : RingElem), forall (b : RingElem), forall (c : RingElem), forall (h : @Eq.{1} RingElem (add a b) (add a c)), @Eq.{1} RingElem b c

Proof term

fun a => fun b => fun c => fun h => @RingElem.rec.{0} (fun (x : RingElem) => @Eq.{1} RingElem x c) (@RingElem.rec.{0} (fun (y : RingElem) => @Eq.{1} RingElem RingElem.unit y) (@Eq.refl.{1} RingElem RingElem.unit) c) b

Constants

Mathlib.Algebra.Ring.RingElem

Interface hash: sha256:29d995d6a38e44a010f577d64428b3272226781f7982e2306784cb3bdc4977ea

Mathlib.Algebra.Ring.add

Interface hash: sha256:70894d2717280dc0e45d28bdc4220a44c51506cccc224ab1f339c97d87eedd41

Std.Logic.Eq.Eq

Interface hash: sha256:ca4f8520fd678a809c3ebf0bc7fa38d3063ca4d231e79d567de888685449a015