Commits leanprover-community/mathlib

chore(order/initial_seg): move definitions of initial and principal segments (#15328)

vihdzp committed 4 years ago

fcceffa0

feat(data/polynomial/unit_trinomial): Irreducibility of X^n-X-1 (#15318)

tb65536 committed 4 years ago

3e63d162

feat(algebra/category): forgetful functors from modules reflect limits (#15095)

TwoFX committed 4 years ago

bada07ee

feat(algebra/homology): homotopy equivalences are quasi-isomorphisms (#14945)

joelriou committed 4 years ago

9f453148

fix(category_theory/abelian/transfer): fix a potential timeout (#15262)

jjaassoonn committed 4 years ago

54594da2

chore(algebra/geom_sum): golf a proof (#15450)

urkud committed 4 years ago

4461149a

feat(measure_theory/function/conditional_expecation): conditional expectation of a function to a independent sigma-algebra (#15422)

kex-y committed 4 years ago

683e1f66

feat(data/nat/bitwise): tweak `lxor` lemmas (#15409)

vihdzp committed 4 years ago

e42057fa

chore(set_theory/zfc): general cleanup (#15208)

vihdzp committed 4 years ago

4dee658e

chore(ring_theory/ideal/operations): golf a lemma (#15431)

eric-wieser committed 4 years ago

7351357b

feat(order/rel_iso): add lemmas on `rel_iso.cast` (#15430)

vihdzp committed 4 years ago

88220853

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

RemyDegenne committed 4 years ago

1b235421

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

vihdzp committed 4 years ago

5a6671a7

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

urkud committed 4 years ago

41e467ac

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

sgouezel committed 4 years ago

d857ca65

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

erdOne committed 4 years ago

a2c2bc99

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

YaelDillies committed 4 years ago

d69acdc9

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

YaelDillies committed 4 years ago

72207732

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

erdOne committed 4 years ago

af5c45db

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

RemyDegenne committed 4 years ago

13e97da3

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

tb65536 committed 4 years ago

ff548cdd

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

eric-wieser committed 4 years ago

9365548b

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

TwoFX committed 4 years ago

3644fef6

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

kex-y committed 4 years ago

6dd5e43c

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

TwoFX committed 4 years ago

b8aa28d3

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

tb65536 committed 4 years ago

57c7d940

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

fpvandoorn committed 4 years ago

3d6c3b6d

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

urkud committed 4 years ago

21a387fe

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

adomani committed 4 years ago

4538aeb2

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

erdOne committed 4 years ago

624716b7