Skip to content

Instantly share code, notes, and snippets.

@vlj

vlj/ring.v

Created March 30, 2020 18:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save vlj/6eeff9466522aaff58d4e48252e9ab7e to your computer and use it in GitHub Desktop.
Save vlj/6eeff9466522aaff58d4e48252e9ab7e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ring.v
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.
Open Scope ring_scope.
Import GRing.Theory.
Variable R: numFieldType.
Lemma tmp:
@ring_theory R 0%:R 1%:R +%R *%R (fun a b => a - b) -%R (fun (x y:R) => x = y).
Admitted.
Add Ring Ringgg : tmp (abstract).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment