Heather Macbeth
Heather Macbeth
Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles --- [](https://gitpod.io/from-referrer/) - [x] depends on: #16475 - [x] depends on: #16476 - [x] depends on: #16477 - [x] depends on: #16478 - [x] depends on:...
This file relates the constructions `orientation.area_form`, `orientation.right_angle_rotation`, `orientation.kahler` on an oriented two-dimensional real inner product space to their concrete interpretations over `ℂ`. --- [](https://gitpod.io/from-referrer/) - [x] depends on:...
--- [](https://gitpod.io/from-referrer/) - [x] depends on: #16928
Construction of the cross-product on an oriented real inner product space of dimension 3. Formalized as part of the Sphere Eversion project. --- [](https://gitpod.io/from-referrer/) - [x] depends on:...
Add constructions `add_equiv.base_at` (of type `perm`), `linear_equiv.base_at` (of type `affine_equiv`), and `linear_isometry_equiv.base_at` (of type `affine_isometry_equiv`), to describe the automorphism of an `add_torsor`/`normed_add_torsor` obtained by fixing a basepoint, temporarily identifying the...
Given a Euclidean affine plane `P` modelled on `ℂ`, I define the type `square_lattice P` of lattices in `P` modelled on the integer lattice in `ℂ`, being careful to do...
A "matrix" of bilinear forms on `M` on a type `α` (possibly infinite) induces a bilinear form on `α →₀ M`, and thence (via `bilin_form.to_quadratic_form` a quadratic form. In particular,...
--- ~~I am opening a PR to get CI to run. I will write an RFC later, informed by the results of CI. I hope this is ok.~~ This is...
In the documentation for [MulEquiv.withOneCongr](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/WithOne/Basic.html#MulEquiv.withOneCongr), the declaration `Equiv.optionCongr` is referenced, but there is no automatic hyperlink to [that declaration](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Option.html#Equiv.optionCongr) in the docs. The [corresponding documentation](https://leanprover-community.github.io/mathlib_docs/algebra/group/with_one/basic.html#mul_equiv.with_one_congr) in doc-gen3 does have the...
If I understand correctly, certain fields that one might want to set in the documentation on a repo-by-repo basis are currently hard-coded in doc-gen4. For example, - the title displayed...