leanprover-community/mathlib3

Pull Requests Commits

refactor(data/polynomial): use `monic.ne_zero` and `nontriviality` (#9530)

Vierkantor committed 4 years ago

15364121

chore(scripts): update nolints.txt (#9553)

leanprover-community-bot committed 4 years ago

fd189536

docs(ring_theory/adjoin_root): fix docstring (#9546)

jcommelin committed 4 years ago

04916217

feat(number_theory/padics): add padic_norm lemmas (#9527)

mariainesdff committed 4 years ago

74664245

fix(order/sub): make arguments explicit (#9541)

fpvandoorn committed 4 years ago

3aac8e5f

feat(set_theory/cardinal,*): assorted lemmas (#9516)

urkud committed 4 years ago

10da8e67

refactor(group_theory/is_p_group): Generalize `is_p_group.comap_injective` (#9509)

tb65536 committed 4 years ago

50b51c5e

feat(data/pnat/interval): Finite intervals in ℕ+ (#9534)

YaelDillies committed 4 years ago

7a5d15a9

feat(order/conditionally_complete_lattice): image and cSup commute (#9510)

YaelDillies committed 4 years ago

e998e4c4

feat(algebra/order/functions): recursors and images under monotone maps (#9505)

YaelDillies committed 4 years ago

d8968ba7

refactor(order/fixed_points): rewrite using bundled `preorder_hom`s (#9497)

urkud committed 4 years ago

fa520678

feat(topology/homotopy): add `homotopy_with` (#9252)

shingtaklam1324 committed 4 years ago

387ff6e3

fix(ci): always use python3 executable (#9531)

gebner committed 4 years ago

f6c77be6

feat(data/fin/interval): Finite intervals in `fin n` (#9523)

YaelDillies committed 4 years ago

a07d1de4

feat(probability_theory/notation): add notations for expected value, conditional expectation (#9469)

RemyDegenne committed 4 years ago

15d987a3

feat(measure_theory/covering/besicovitch_vector_space): vector spaces satisfy the assumption of Besicovitch covering theorem (#9461)

sgouezel committed 4 years ago

ab7d2519

feat(analysis/special_functions): real derivs of `complex.exp` and `complex.log` (#9422)

urkud committed 4 years ago

b6f94a93

feat(ring_theory/algebraic_independent): Existence of transcendence bases and rings are algebraic over transcendence basis (#9377)

ChrisHughes24 committed 4 years ago

1faf964e

feat(order/jordan_holder): Jordan Hölder theorem (#8976)

ChrisHughes24 committed 4 years ago

8a05dca7

feat(linear_algebra/matrix/general_linear_group): GL(n, R) (#8466)

CBirkbeck committed 4 years ago

abe81bcb

feat(topology/algebra): nonarchimedean filter bases (#9511)

PatrickMassot committed 4 years ago

edb22fef

feat(data/nat/interval): finite intervals of naturals (#9507)

YaelDillies committed 4 years ago

6bd6afaf

feat(linear_algebra/free_module/strong_rank_condition): add `comm_ring_strong_rank_condition` (#9486)

riccardobrasca committed 4 years ago

dc1b045a

feat(category_theory/sites/*): Cover-lifting functors on sites (#9431)

erdOne committed 4 years ago

6a6b4d05

feat(field_theory/algebraic_closure): versions of exists_aeval_eq_zero for rings (#9517)

ChrisHughes24 committed 4 years ago

d677c298

chore(data/set/lattice): fix name (#9520)

sgouezel committed 4 years ago

52495a0f

split(order/monotone): split off `order.basic` (#9518)

YaelDillies committed 4 years ago

465508fc

feat(algebra/order): exists_square_le (#9513)

PatrickMassot committed 4 years ago

c0f7c56e

feat(topology/algebra): Cauchy filters on groups (#9512)

PatrickMassot committed 4 years ago

bc5a081f

chore(*): use dot-notation for is_conj.symm and is_conj.trans (#9498)

jcommelin committed 4 years ago

44f4d708

Newer Older