Joseph Myers
Joseph Myers
Add a lemma about the sign of the product of two numbers (in the `linear_ordered_ring` case, deduced from the existing `sign_hom` in that case). --- [](https://gitpod.io/from-referrer/)
Add lemmas that two vectors are linearly dependent if and only if they are in the same ray or one is in the same ray as the negation of the...
We have various lemmas giving conditions for an angle to equal 0 or π. Add some more such lemmas, plus negated versions of existing lemmas giving conditions for angles not...
Define `real.angle.to_real`, converting a `real.angle` to a real in the interval `Ioc (-π) π` (the same interval used by `complex.arg`), and prove some associated lemmas. This is the inverse operation...
Make `geometry.euclidean` files consistently use notation for the inner product, rather than mixing notation with non-notation calls to `inner`. Also always get that notation from `open_locale real_inner_product_space` instead of a...
Add lemmas that, in a real normed space, the sets of points on the same side of an affine subspace as a given point, or on the opposite side from...
Special-case use of HTML tags for `sub_symbol` and `sup_symbol`. In particular, this allows setting `sub_symbol=''`, `sup_symbol=''` to use raw HTML in the output when converting subscripts and superscripts.
There are various cases in which inline text fails to be separated by (sufficiently many) newlines from adjacent block content. A paragraph needs a blank line (two newlines) separating it...
IEEE 754, TR 24732 and TS 18661-2 all specify that conversions between binary and decimal floating point types, in either direction, must be correctly rounded. The libdfp conversions, however, are...
At least some libdfp conversions between decimal and binary types wrongly always produce a zero for obvious underflowing results, without taking account of the rounding mode (the relevant rounding mode...