Package: wnpp Severity: wishlist Owner: Riley Baird <bm-2cvqnduybau5do2dfjtrn7zbaj246s4...@bitmessage.ch>
* Package name : coq-highschoolgeometry Version : 8.4+20150620 Upstream Author : Frédérique Guilhot <frederique.guil...@sophia.inria.fr> * URL : http://www.lix.polytechnique.fr/coq/pylons/coq/pylons/contribs/view/HighSchoolGeometry/trunk * License : LGPL-2.1+ Programming Lang: Coq Description : coq library for high school geometry proofs/formalisation Created by Frédérique Guilhot, this library consists of a collection of "chapters" spanning most of the geometry taught in French high schools. The first part "2-3 dimensional affine geometry" deals with formalising: points, vectors, barycenters, oriented lengths collinearity, coplanarity parallelism and incidence of straight lines proofs of Thales and Desargues theorems. In the second part "3 dimensional affine geometry", we prove theorems about: relative positions of two straight lines in the space relative positions of a straight line and a plane relative positions of two planes parallelism and incidence properties for several planes and straight lines The third part "2-3 dimensional euclidean geometry" deals with formalising: scalar product, orthogonal vectors, and unitary vectors Euclidean distance and orthogonal projection on a line proofs of Pythagorean theorem, median theorem The fourth part "space orthogonality" deals with formalising: orthogonal line and plan The fifth part "plane euclidean geometry" deals with formalising: affine coordinate system, orthogonal coordinate system, affine coordinates oriented angles trigonometry proofs of Pythagorean theorem, median theorem, Al-Kashi and sine theorems perpendicular bisector, isocel triangle, orthocenter circle, cocyclicity, tangency (line or circle tangent) signed area, determinant equations for straight lines and circles in plane geometry The sixth part "plane transformations", deals with formalising: translations, homothety rotations, reflexions composition of these transformations. conservation of tangency for these transformations. In the seventh part "applications", we prove: Miquel's theorem, orthocenter theorem, Simson line circle power and plane inversion Euler line theorem and nine point circle theorem The eighth part "complex numbers", deals with formalising: the field properties of complex numbers application to geometry of complex numbers This package is a dependency of geoproof. -- To UNSUBSCRIBE, email to debian-devel-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: https://lists.debian.org/20150620232033.6879.50974.reportbug@debian.fleetstreet
