mathlib

mathlib copied to clipboard

Co-authored-by: Jujian Zhang --- Rewrite of a result from #15954. [](https://gitpod.io/from-referrer/)

Ruben-VandeVelde

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...

jsm28

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...

jsm28

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ

2

This refactors `pi_Lp` so that the `p` argument has type ℝ≥0∞ instead of ℝ. There are several reasons for doing this: 1. It matches the design of `lp`. 2. We...

j-loreaux

feat(topology/algebra/uniform_ring): ring completions and algebra structures

6

If `A` is an algebra over `R`, so is the `uniform_space.completion` of `A`. --- - [x] depends on: #14846 [](https://gitpod.io/from-referrer/)

mariainesdff

feat(category_theory): compute subobjects of structured arrows

1

One step closer to the Special Adjoint Functor Theorem. --- - [x] depends on: #15494 - [ ] depends on: #16050 [](https://gitpod.io/from-referrer/)

TwoFX

--- Split off from #15912 to reduce merge conflicts with a future PR. [](https://gitpod.io/from-referrer/)

TwoFX

feat(set_theory/cardinal): cardinality of `multiset`, `polynomial` and `mv_polynomial`

4

+ Show `#(multiset α) = max (#α) ℵ₀` when `α` is nonempty. Show the same for `#(α →₀ ℕ)`, which is used in the mv_polynomial proof (see below). + Prove...

alreadydone

feat(data/*): `unique` instances for `dfinsupp` and `direct_sum`

11

+ Add `unique` instances when the codomain types are subsingletons and rename the original `unique` instances (which apply when the domain is empty) to `unique_of_is_empty`. These are in analogy to...

alreadydone

feat(ring_theory/localization/away): R[X]/(rX-1) as localization

5

I don't have any specific application in mind, and just wanted to test how hard it is to connect the two. For a general submonoid, adjoining the inverses of elements...

alreadydone