mathlib

mathlib copied to clipboard

feat(algebra/category/Module/change_of_rings): extension of scalars

5

Given a ring homomorphism $f : R \to S$ between commutative rings, the extension of scalars functor from $R$-module to $S$-module. In #15564 it will proven that extension of scalars...

jjaassoonn

feat(group_theory/divisible): definition of divisible group

9

This PR defines divisible group and proves that the set of rationals is divisible and product of divisible group is divisible. Future PR will be opened to prove that divisibility...

jjaassoonn

feat(analysis/transcendental): e is transcendental

1

--- #3884, second attempt. [](https://gitpod.io/from-referrer/)

Ruben-VandeVelde

* replace `*_hom.map_inv` by a generic lemma `map_inv₀` assuming `[monoid_with_zero_hom_class]`; * replace `*_hom.map_div` by a generic lemma `map_div₀` assuming `[monoid_with_zero_hom_class]`; * replace `*_hom.map_zpow` by a generic lemma `map_zpow₀` assuming `[monoid_with_zero_hom_class]`;...

urkud

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

1

--- - [ ] depends on: #14857 - [ ] depends on: #16052 - [ ] depends on: #16054 [](https://gitpod.io/from-referrer/)

ADedecker

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint`

4

We rename the current `inner_product_space.is_self_adjoint` to `linear_map.is_symmetric` (which states that `inner (A x) y = inner x (A y)` for all `x,y : E`) and add a new definition `is_self_adjoint`...

mcdoll

feat(topology/algebra/uniform_convergence): maps to a uniform group form a uniform group when equipped with the uniform structure of `𝔖`-convergence

1

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

ADedecker

feat(topology/uniform_space/uniform_convergence_topology): bases for uniform structures of 𝔖-convergence

1

By definition, the sets `S(V) := {(f, g) | ∀ x, (f x, g x) ∈ V}` for `V∈𝓤 β` form a basis for the uniformity of uniform convergence on...

ADedecker

feat(topology/algebra/uniform_convergence): criterion for a vector subspace of `α → E` to be a TVS for the topology of 𝔖-convergence

1

The main theorem is `uniform_convergence_on.has_continuous_smul_induced_of_image_bounded`. As explained in the module docstring, one could get rid of requiring `𝔖` to be nonempty and directed, but the easiest way to get that...

ADedecker

feat(measure_theory/measure/finite_measure_weak_convergence): Add portmanteau implications concerning open and closed sets.

1

Add equivalence of a limsup condition for closed sets and a liminf condition for open sets, which will later both be shown to be characterizing conditions of weak convergence of...

kkytola