mathlib

mathlib copied to clipboard

feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category

8

We generalise the [well-known construction](https://ncatlab.org/nlab/show/bimodule#AsMorphismsInA2Category) of the 2-category of rings, bimodules, and intertwiners. Given a monoidal category `C` that has coequalizers and in which left and right tensor products preserve...

manzyuk

Pi is irrational

5

Prove that `real.pi` is irrational using [Niven's argument](https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society/volume-53/issue-6/A-simple-proof-that-pi-is-irrational/bams/1183510788.full), see also [Wikipedia](https://en.wikipedia.org/wiki/Proof_that_%CF%80_is_irrational#Niven's_proof) [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Paulson's.20.22small.20formalisation.20challenges.22)

mcdoll

feat(category_theory/category/Pointed): `Pointed` is a monoidal category

1

Provide the `monoidal_category` and `symmetric_category` instances for `Pointed`. --- This is mostly an exercise for me to see whether I understand monoidal categories. Please suggest missing API. I tried to...

YaelDillies

feat(algebra/jordan/special): Introduce special Jordan algebras

1

A commutative multiplication on a real or complex space can be constructed from any multiplication by "symmetrisation" i.e ``` a∘b = 1/2(ab+ba). ``` When the original multiplication is associative, the...

mans0954

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring

7

Define the centroid of a (non-unital, non-associative) semiring and shows that it forms a semiring. The centroid of a (non-unital, non-associative) ring is a ring. When the ring is prime,...

mans0954

feat(combinatorics/additive/ruzsa_szemeredi): The Ruzsa-Szemerédi problem

2

Prove the (implicit) lower bound on the Ruzsa-Szemerédi problem. --- We can prove the explicit bound once #15327 is merged. Bhavik told me to golf the proof using https://github.com/leanprover-community/mathlib/blob/1874b7ab2089c2c9922e89026527b9806f2d0953/src/combinatorics/szemeredi/triangle.lean#L349-L365 but...

YaelDillies

feat(analysis/normed/ring_seminorm): add ring_seminorm, ring_norm

13

We define structures `ring_seminorm` and `ring_norm`. These definitions are useful when one needs to consider multiple (semi)norms on a given ring. --- [](https://gitpod.io/from-referrer/)

mariainesdff

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID

1

A definition plus some extra lemmas about PIDs that will be used in #15000 --- [](https://gitpod.io/from-referrer/)

Paul-Lez

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms

1

This PR provides the proof that every locally convex space has a family of seminorms that induces the topology. This PR also adds a new simp-lemma `is_R_or_C.real_norm`, which calculates the...

mcdoll

feat(number_theory/miller_rabin): adding lemmas about the miller rabin primality test.

1

Added a couple of lemmas and definitions that will be used in proving the Miller-Rabin primality test. --- - [x] depends on: #12973 - [x] depends on: #12989 [![Open in...

seangolinski7