leanprover-community/mathlib

Pull Requests Commits

dwarn committed 3 years ago

b785cdda

dwarn committed 3 years ago

0443eb37

Merge remote-tracking branch 'origin/master' into deuber

dwarn committed 3 years ago

8fbae22e

chore(algebra/ne_zero): revert transitivity changes (#11760)

ericrbg committed 3 years ago

4db1f964

feat(group_theory/subgroup/basic): normalizer condition implies max subgroups normal (#11597)

nomeata committed 3 years ago

6c6fbe66

feat(group_theory/nilpotent): p-groups are nilpotent (#11726)

nomeata committed 3 years ago

1ed19a9d

feat(measure_theory/probability_mass_function): Measures of sets under `pmf` monad operations (#11613)

dtumad committed 3 years ago

c1d28601

feat(field_theory/intermediate_field, ring_theory/.., algebra/algebra… (#11168)

Sebastian-Monnet committed 3 years ago

a687cbfb

chore(ring_theory/power_basis): add `simps` (#11766)

ericrbg committed 3 years ago

d5d57849

refactor(power_series/basic): generalize order to semirings (#11765)

pechersky committed 3 years ago

2fdc1510

feat(group_theory/p_group): p-groups with different p are disjoint (#11752)

nomeata committed 3 years ago

a32b0d37

feat(group_theory/subgroup/basic): add commute_of_normal_of_disjoint (#11751)

nomeata committed 3 years ago

664b5bed

feat(order/category/*): `order_dual` as an equivalence of categories (#11743)

YaelDillies committed 3 years ago

a6d70aa7

refactor(ring_theory/non_zero_divisors): use fun_like (#11764)

pechersky committed 3 years ago

400dbb3a

chore(measure_theory/covering/besicovitch): Weaker import (#11763)

vihdzp committed 3 years ago

c8fd7e33

chore(topology/continuous_function/ordered): split from `continuous_function/basic` (#11761)

hrmacbeth committed 3 years ago

a18680a6

feat(analysis/special_functions): show (2 / π) * x ≤ sin x (#11724)

b-mehta committed 3 years ago

366fd9b1

feat(topology/homotopy): Fundamental groupoid preserves products (#11459)

prakol16 committed 3 years ago

5c4c1c08

chore(*): Golfed some random theorems (#11769)

vihdzp committed 3 years ago

fa863706

feat(measure_theory/measure): drop more `measurable_set` args (#11547)

urkud committed 3 years ago

8ef783b4

chore(linear_algebra): remove `bilinear_map` from imports in `pi` (#11767)

mcdoll committed 3 years ago

d68b4808

feat(sites/sheaf): simple sheaf condition in terms of limit (#11692)

alreadydone committed 3 years ago

343cbd98

feat(algebra/group_power): relate square equality and absolute value equality (#11683)

b-mehta committed 3 years ago

ec611821

chore(*): register global fact instances (#11749)

sgouezel committed 3 years ago

23e0e290

feat(model_theory/basic.lean): Elementary embeddings and elementary substructures (#11089)

awainverse committed 3 years ago

2508cbd9

chore(set_theory/ordinal_arithmetic): Remove redundant explicit argument (#11757)

vihdzp committed 3 years ago

94a700f3

feat(set_theory/ordinal_arithmetic): Normal functions evaluated at `ω` (#11687)

vihdzp committed 3 years ago

ca2a99dd

feat(set_theory/{ordinal_arithmetic, cardinal_ordinal}): Ordinals aren't a small type (#11756)

vihdzp committed 3 years ago

cbad62c5

feat(number_theory/cyclotomic/zeta): add lemmas (#11753)

riccardobrasca committed 3 years ago

30dcd70e

feat(data/two_pointing): Two pointings of a type (#11648)

YaelDillies committed 3 years ago

350ba8db

Older