isabelle: src/HOL/Complex/NSComplexArith.thy@c817dd885a32 (annotated)

14326 c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	1	(* Title: NSComplexArith
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	2	Author: Lawrence C. Paulson
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	3	Copyright: 2003 University of Cambridge
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	4
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	5	Common factor cancellation
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	6	*)
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	7
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	8	theory NSComplexArith = NSComplexBin
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	9	files "hcomplex_arith.ML":
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	10
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	11	subsubsection{Division By @{term "-1"}}
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	12
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	13	lemma hcomplex_divide_minus1 [simp]: "x/-1 = -(x::hcomplex)"
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	14	by simp
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	15
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	16	lemma hcomplex_minus1_divide [simp]: "-1/(x::hcomplex) = - (1/x)"
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	17	by (simp add: hcomplex_divide_def hcomplex_minus_inverse)
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	18
c817dd885a32 reorganised complex arithmetic paulson parents: diff changeset	19	end

author	paulson
	Tue, 23 Dec 2003 18:26:03 +0100
changeset 14326	c817dd885a32
child 14335	9c0b5e081037
permissions	-rw-r--r--