mathlib

mathlib copied to clipboard

We have a diamond of complete boolean algebras on sets: ```lean import data.set.lattice variables {α : Type*} -- Succeeds example : @set.boolean_algebra α = pi.boolean_algebra := rfl -- Fails example...

ocfnash

--- [](https://gitpod.io/from-referrer/)

jjaassoonn

refactor(algebra/order/floor): Relax lemmas to remove `linear_order` requirement

13

There is a TODO in `algebra/order/floor.lean` which notes that many lemmas do not require the linearly ordered part of their hypothesis and these could be relaxed. This commit actions this...

linesthatinterlace

feat(topology/algebra/module/locally_convex): generalize `disjoint.exists_open_convexes` to locally convex spaces

1

--- - [x] depends on: #16747 [](https://gitpod.io/from-referrer/)

ADedecker

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces

1

--- - [ ] depends on: #16782 - [ ] depends on: #16749 [](https://gitpod.io/from-referrer/)

ADedecker

feat(number_theory/modular_forms): Modular form definition

14

This contains the basic definitions of modular forms and cusp forms together with some lemmas about mdifferentiability that are needed. --- - [x] depends on: #15009 [](https://gitpod.io/from-referrer/)

CBirkbeck

feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons

2

This establishes the correspondence between maximal ideals of `C(X, 𝕜)` (where `X` is compact Hausdorff and `is_R_or_C 𝕜`) and the complements of singletons in `X`. This allows for the proof...

j-loreaux

feat(tactic/print_sorry): add `#print_sorry_in` command

2

Note: This command will happily print internal declarations like `foo._proof_i`. You could make it a bit nicer by not printing these as separate declarations, but the current version is already...

fpvandoorn

feat(topology/algebra/module/basic): a hyperplane is either closed or dense

1

--- - [x] depends on: #16786 [](https://gitpod.io/from-referrer/)

ADedecker

feat(analysis/normed_space/lp_space): "functoriality" of `lp`

1

--- [](https://gitpod.io/from-referrer/)

ADedecker