mathlib

mathlib copied to clipboard

homological algebra

4

We'd like to have the basics of homological algebra (complexes, chain maps, homotopy equivalences, exact sequences, homology). There will be some overlap with the theory of simplicial objects: this issue...

kim-em

Goals `a ≠ b` turn up quite often when working over general fields, notably goals `a ≠ 0` to allow for the use of `field_simp` with a denominator `a`. Often...

hrmacbeth

A Lipschitz function from a subset of a space into ℓ^∞ can be extended to the whole space, with the same Lipschitz constant. See Theorem 2.2 here: https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf We have...

hrmacbeth

Right now `to_ring_hom_eq_coe` is not a simp lemma, which makes it not possible to deduce something like `(f : R ≃+* S) : ⇑(f.to_ring_hom) = ⇑f` by `simp`. The open...

mcdoll

`partial_order.lift` vs `function.injective.partial_order`

1

> Should we rename `partial_order.lift` to `function.injective.partial_order`? Or conversely, should the definitions in this PR be called `lattice.lift` etc? It might be worth polling on Zulip. _Originally posted by @eric-wieser...

eric-wieser

The idea would be to have an attribute to force a theorem to avoid classical logic, which would detect regressions caused by classical simp lemmas unexpectedly firing. [From Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/intuitionistic.20logic/near/224368423): ```lean...

eric-wieser

suggest and show_term give incorrect suggestions

7

Uncomment each block of code one at a time: ```lean import data.real.basic import data.set.basic -- library_search fails -- example : ∃ (s : set ℝ), ∀ (r : ℝ), r...

ghost

documenting mathlib

2

We have instituted [new documentation requirements](https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/doc.md) for mathlib additions: https://github.com/leanprover-community/mathlib/pull/1229 It is a long term effort to bring the existing mathlib code base up to these standards. New pull requests...

robertylewis

`ext` recurses into subgoals, `ext x y z` and `ext : n` do not

2

Reproduction (on mathlib 8fd86366a4472716b25100e831a2ba0f266b28b8) ```lean import linear_algebra.basic variables {R : Type*} {M : Type*} {M₂ : Type*} {M₃ : Type*} {M₄ : Type*} variables [semiring R] variables [add_comm_monoid M] [add_comm_monoid...

eric-wieser

Consider the following MWE: ```lean import tactic.fin_cases example (a x : ℕ) (hx : x ∈ ({a, a} : finset ℕ)) : x = a := begin fin_cases hx, --...

alexjbest