mathlib

mathlib copied to clipboard

feat(data/real/dedekind_cut): define and add_comm_group

5

Based on Principles of mathematical analysis by Rudin TODO: finish proving they form a field, and are isomorphic to the reals. --- [](https://gitpod.io/from-referrer/)

pechersky

feat(algebra/module/submodule/lattice): `submodule.is_maximal`

3

This PR replaces the previous typeclass for maximal left ideals `ideal.is_maximal : ideal R -> Prop` with `submodule.is_maximal : submodule R M -> Prop`, which is a typeclass for maximal...

haruhisa-enomoto

--- Add formalization and proofs for time complexity of insertion_sort and merge_sort, as discussed [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/BSc.20Final.20Project/near/220647062) and [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Formalization.20of.20Runtime.20Complexity.20of.20Sorting.20Algorithms/near/284184450). Reference (pt-br): https://github.com/tomaz1502/RunTimeFormalization/blob/main/Report.pdf [](https://gitpod.io/from-referrer/)

tomaz1502

feat(ring_theory/valuation/valuation_subring): Supremum of families of valuation rings.

1

Adds two definitions: - The supremum of a directed family of valuation rings, as a valuation ring. - The supremum of a family of valuation rings which are bounded below...

adamtopaz

This aims to generalize some of the `nnreal_binary` stuff in LTE. https://github.com/leanprover-community/lean-liquid/blob/b9b42a840d2416657d7ba173f5d20e24906e6137/src/for_mathlib/nnreal_int_binary.lean#L136-L140 --- [](https://gitpod.io/from-referrer/)

eric-wieser

refactor(linear_algebra/clifford_algebra): relax typeclasses to semiring

1

This generalization isn't motivated by any particular result or generalization in the literature; rather, it's motivated by allowing `exterior_algebra R M` to be redefined as `clifford_algebra 0`, as this prevents...

eric-wieser

feat(measure_theory/integral/lebesgue): add a lemma

2

A `lintegral` version of a lemma from @sgouezel's #13690. --- - [x] depends on: #14293 - [x] depends on: #14294 - [x] depends on: #14296 [](https://gitpod.io/from-referrer/)

urkud

Provide a way to convert NFAs to regular expressions and vice versa, and prove that the conversions accept the same language. TODO: statement of some theorems, style, adding @[simp] annotations...

RussellEmerine

Construction of a basis that triangulates a nilpotent linear map. --- [](https://gitpod.io/from-referrer/) I plan to use this result to triangularize more general matrices.

abentkamp

A few basic lemmas and definitions, with a few special cases for the projective line (as `P K (K \times K`). --- [](https://gitpod.io/from-referrer/)

vbeffara