Commits leanprover-community/mathlib

feat(measure_theory/integral): generalize some integral properties to set_to_fun (#15423)

RemyDegenne committed 3 years ago

1b235421

chore(order/basic): remove two lemmas breaking API boundaries (#15401)

vihdzp committed 3 years ago

5a6671a7

feat(analysis/complex/abs_max): add a version of the maximum modulus principle (#15364)

urkud committed 3 years ago

41e467ac

feat(analysis/calculus/mean_value): remove assumption in strict_mono_on.strict_convex_on_of_deriv (#15133)

sgouezel committed 3 years ago

d857ca65

feat(topology/noetherian_space): Noetherian spaces (#14965)

erdOne committed 3 years ago

a2c2bc99

feat(data/finset/powerset): More `powerset` lemmas (#15387)

YaelDillies committed 3 years ago

d69acdc9

feat(group_theory/group_action/option): Scalar action on an option (#15239)

YaelDillies committed 3 years ago

72207732

feat(algebraic_geometry): Restriction of morphisms onto open sets of the target (#14972)

erdOne committed 3 years ago

af5c45db

chore(measure_theory/tactic): fix a loop in the measurability tactic (#14813)

RemyDegenne committed 3 years ago

13e97da3

feat(field_theory/adjoin): `F⟮α⟯ ≤ K ↔ α ∈ K` (#15420)

tb65536 committed 3 years ago

ff548cdd

feat(group_theory/submonoid/pointwise): add the pointwise monoid structure on `add_submonoid` (#15052)

eric-wieser committed 3 years ago

9365548b

chore(category_theory): enough_injectives is dual to enough_projectives (#15395)

TwoFX committed 3 years ago

3644fef6

feat(measure_theory/function/uniform_integrable): conditional expectations form a uniformly integrable class (#15378)

kex-y committed 3 years ago

6dd5e43c

feat(category_theory): limits of essentially small indexing categories (#15377)

TwoFX committed 3 years ago

b8aa28d3

feat(field_theory/adjoin): The compositum of finitely many finite dimensional intermediate fields is finite dimensional (#15339)

tb65536 committed 3 years ago

57c7d940

feat(geometry/manifold|topology): add simps and ext attributes (#15314)

fpvandoorn committed 3 years ago

3d6c3b6d

feat(algebra/order/monoid_lemmas): add `antitone`, `monotone_on`, and `antitone_on` lemmas (#15267)

urkud committed 3 years ago

21a387fe

feat(data/finset/fold): add lemma `fold_max_add` (#15257)

adomani committed 3 years ago

4538aeb2

feat(ring_theory/tensor_product): `A`-algebra structure on `A' ⊗[R] B`. (#15241)

erdOne committed 3 years ago

624716b7

feat(order/filter): add `map_neg_at_top`, change some assumptions (#15237)

urkud committed 3 years ago

316d1886

feat(algebra/gcd_monoid): GCD domains are integrally closed. (#15109)

erdOne committed 3 years ago

511a9f79

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas about typeclasses (#14761)

astrainfinita committed 3 years ago

9becea2d

fix(tactic/solve_by_elim): apply_assumption argument parsing (#15394)

robertylewis committed 3 years ago

367714d6

feat(data/json): helper functions for json serialization (#15207)

eric-wieser committed 3 years ago

8963fcfc

chore(number_theory/number_field): remove duplicate name (#15400)

ericrbg committed 3 years ago

45e412da

feat(order/bounded_order): two lemmas about the interaction between monotonicity and map with_bot/top (#15341)

adomani committed 3 years ago

ced11136

feat(data/countable): add `countable` typeclass (#15280)

urkud committed 3 years ago

68123285

feat(ring_theory/power_series/basic): Add `rescale_X` (#15397)

tyler-billingsley committed 3 years ago

2dbbe579

feat(measure_theory/measure/finite_measure_weak_convergence): Add some missing API lemmas. (#15205)

kkytola committed 3 years ago

dc7ab9e7

feat(group_theory/group_action/sub_mul_action): add the pointwise monoid structure (#15050)

eric-wieser committed 3 years ago

7c54be86