Commits leanprover-community/mathlib3

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

feat(category_theory): (co)products and (co)separators (#14880)

TwoFX committed 3 years ago

884dde3b

feat(data/vector/basic): make the recursor work with `induction _ using` syntax (#15383)

eric-wieser committed 3 years ago

f23205e9

feat(data/sum/basic): `sum.lift_rel` is a subrelation of `sum.lex` (#15358)

vihdzp committed 3 years ago

b560d401

feat(set_theory/zfc): more `quotient` lemmas (#15324)

vihdzp committed 3 years ago

7929a63e

chore(analysis/locally_convex): golf a proof (#15323)

urkud committed 3 years ago

15da6257

feat(analysis/special_functions/polar_coord): define polar coordinates, polar change of variable formula in integrals (#15258)

sgouezel committed 3 years ago

959586cf

chore(ring_theory/ideal/operations): generalise some typeclasses (#15200)

alexjbest committed 3 years ago

f6e9ec38

feat(linear_algebra/linear_pmap): construct a `linear_pmap` from its graph (#14922)

mcdoll committed 3 years ago

9c8bc915

feat(data/finset/basic): lemmas about `filter`, `cons`, and `disj_union` (#15385)

eric-wieser committed 3 years ago

ecaa2891