mathlib

mathlib copied to clipboard

feat(algebra/monoid_algebra/degree): add definitions of `degree`s of add_monoid_algebras

26

This PR defines 1. the `sup_degree` of an `add_monoid_algebra`, graded by a `semilattice_sup`; 1. the `inf_degree` of an `add_monoid_algebra`, graded by a `semilattice_inf`; 1. the `max_degree` of an `add_monoid_algebra`, graded...

adomani

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies

18

* Remove the `t2_space` assumption from `exists_compact_between` by generalizing the proof of `exists_compact_superset`, and move it from `topology/separation` to `topology/subset_properties`. * Use it to prove `continuous_map.continuous_prod` in `topology/continuous_map` stating that...

faenuccio

Define `real.angle.to_real`, converting a `real.angle` to a real in the interval `Ioc (-π) π` (the same interval used by `complex.arg`), and prove some associated lemmas. This is the inverse operation...

jsm28

This contains the definition of a congruence subgroup of `SL(2,Z)` and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them. --- [](https://gitpod.io/from-referrer/)

CBirkbeck

feat(analysis/complex/upper_half_plane): Functions bounded at infinity

4

The defines the notion of functions on the upper half plane being bounded at infinity and zero at infinity. This is required for #13250. --- [](https://gitpod.io/from-referrer/)

CBirkbeck

feat(combinatorics/simple_graph/triangle/basic): add ε-triangle-free far graph predicate

6

Define the property of being triangle-free far. This comes up in the triangle counting and triangle removal lemmas. Co-authored-by: Bhavik Mehta --- - [x] depends on: #12982 - [x] depends...

YaelDillies

Lean is unable to automatically infer `ordered_smul` instance for `fin n → ℝ` from [docs#ordered_smul'](https://leanprover-community.github.io/mathlib_docs/algebra/order/module.html#pi.ordered_smul'). This in turns leads to issues with defining the [docs#convex_cone.positive](https://leanprover-community.github.io/mathlib_docs/find/convex_cone.positive) in these vector spaces. [Zulip...

apurvnakade

feat(analysis/convex/cone): dual_of_dual_eq_self

1

Proof that the dual of dual of a closed convex cone is itself. I'll break this result into smaller PRs. This result is fundamental to formalising linear (or rather conic)...

apurvnakade

feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min'

2

The six lemmas in this PR show that * `finset.max` and `finset.max'` coincide (when and how they can); * the `finset.max'` of `s.erase x` is not `x`; * the `finset.max`...

adomani

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

vihdzp