mathlib

mathlib copied to clipboard

`expand_exists` improvements

1

Reported by @RemyDegenne on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/expand_exists.20questions): > I am testing the new `expand_exists` attribute, which looks like a very useful tool, and I have two remarks/questions: > - The names given...

robertylewis

We have the definition of locally convex spaces and the characterization of locally convex spaces via seminorms. We have all the ingredients to prove the very useful lemma: Let X...

mcdoll

properties of (sub)modules

1

- [x] finite - [x] finitely generated (done for submodules, we might want a wrapper to make life easier when working with a full module) (#4634) - [ ] finitely...

jcommelin

We are missing instances `add_submonoid_class S M → has_coe S (add_submonoid M)` (probably `has_coe_t` now that I think of it), so we can just use `coe` [here](https://github.com/leanprover-community/mathlib/pull/14583#discussion_r907373588_). Similar coercions should...

Vierkantor

Example ```lean import tactic.apply import data.set.basic example {α : Type*} (a b : set α) : a ⊆ b := by refl' -- closes the goal -- by apply' set.subset.refl...

fpvandoorn

In the following example, `nth_rewrite` incorrectly instantiates the universe metavariable of `h` with `0`, but still rewrites with the hypothesis. Note that `rw` does this correctly. ```lean def foo (h...

fpvandoorn

PR #11246 defines `real.logb`: the logarithm base `b`. Many lemmas about this are provided in `analysis/special_functions/logb.lean`, roughly analogous to the lemmas for the natural logarithm in `analysis/special_functions/log.lean`. But lemmas about...

BoltonBailey

Approximation tactic

1

I don't know anything about the implementation of `norm_num`, but in my ideal world, these lemmas would entirely be handled by `norm_num`. _Originally posted by @Smaug123 in https://github.com/leanprover-community/mathlib/issues/8002#issuecomment-1158021087_ There are...

BoltonBailey

The long line

4

[The long line](https://en.wikipedia.org/wiki/Long_line_(topology)) is often used as a counterexample in topology. It can be defined as `lex ℝ (Ico (0 : ℝ) 1)` which is already equipped with its order...

YaelDillies

Create library note explaining seemingly redundant `fintype` and `decidable` arguments.

1

Although `fintype` and `decidable` are (sub)singletons, since different instances are not definitionally equal, it's useful to have instance arguments that are seemingly redundant. For example: ```lean lemma to_finset_inter {α :...

kmill