mathlib

mathlib copied to clipboard

Get rid of `is_(semi)ring_hom`

4

Unbundled homomorphisms are deprecated but are still used in many files. Here is the output of `git grep -l 'is_\(semi\)\?ring_hom'` with my comments: * `src/algebra/direct_limit.lean` * `src/algebra/field.lean` :: only used...

urkud

More on quotients of categories

2

In `category_theory.quotient` we currently have a construction of the quotient of a category by an arbitrary relation on the Hom-sets, and half of its universal property (we could also prove...

rwbarton

Define exact sequences

3

The usual definition of exactness in category theory seems to be along the lines of "the image of `f` is a kernel of `g`". I have found this definition to...

TwoFX

* [ ] port convexity to vector spaces (`[module 𝕜 E]`) - [x] redefine `segment` and `open_segment` - [x] redefine `convex` - [x] redefine `convex_on` and `concave_on` - [ ]...

urkud

"simp normal form" should be documented

1

In order to make effective use of the simplifier, among all the syntactically distinct propositionally equal / definitionally equal forms of some expression, we try to choose one that is...

bryangingechen

Suggested by @PatrickMassot in https://github.com/leanprover-community/mathlib/pull/7684#issuecomment-846377641

bryangingechen

The `@[elementwise]` attribute creates a copy of a category-theory lemma which essentially applies `(forget C).map` to both sides of an equation, then applies it to an arbitrary element. This gives...

kim-em

Following on from #6820 and the discussion in https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Simplicial.20stuff. We have a construction for Kan extensions from the existence of certain (co)limits over (co)structured arrow categories, but Kan extensions can...

b-mehta

E.g. ``` import tactic.basic reserve notation `#file_decls` -- examples lemma bar (n : ℕ) (h1 : 0 < n) : 0 < n := sorry lemma baz (n : ℕ)...

alexjbest

`ext` on structures should use `subsingleton` instances to avoid unnecessary hypotheses

1

Toy example: ```lean import tactic.ext @[ext] structure foo (α : Type*) := (a : α) (b : unit) #check @foo.ext ``` The generated lemma has type `foo.ext : ∀ {α...

rwbarton