leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/monoid_algebra/{ basic + support } + import dust): move lemmas to a new "support" file (#16322)

adomani committed 3 years ago

20cfd341

feat(analysis/complex/basic): add `complex.ring_hom_eq_id_or_conj_of_continuous` (#16169)

xroblot committed 3 years ago

489c1c57

feat(order/filter/basic): add `eventually_le.add_le_add` (#16295)

kex-y committed 3 years ago

f5da0822

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

leanprover-community-bot committed 3 years ago

5083718c

chore(.github/workflows): increase olean generation timeout (#15784)

collares committed 3 years ago

13618c1c

feat(category_theory/limits): (co)limits in full subcategories (#16188)

TwoFX committed 3 years ago

fe5e4ce6

feat(probability/hitting_time): add some hitting time lemmas (#16296)

kex-y committed 3 years ago

002aa517

feat(data/polynomial/derivative): add more lemmas (#16139)

Ruben-VandeVelde committed 3 years ago

1da31fac

chore(analysis, measure_theory): Fix lint (#16216)

YaelDillies committed 3 years ago

d003c550

chore(*): bump to lean 3.47.0 (#16252)

digama0 committed 3 years ago

3d7987cd

feat(linear_algebra/finite_dimensional): `dim_add_le_dim_add_dim` (#16301)

jsm28 committed 3 years ago

fbfe26dc

feat(algebraic_topology): the category simplicial_object.split (#16274)

joelriou committed 3 years ago

86e93623

feat(category_theory/adjunction): the Special Adjoint Functor Theorem (#15987)

TwoFX committed 3 years ago

c82fab81

feat(data/list/rdrop): drop or take from the right (#15475)

pechersky committed 3 years ago

ed231516

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

leanprover-community-bot committed 3 years ago

3683b34a

feat(ring_theory/unique_factorization_domain): add `associated_iff_normalized_factors_eq_normalized_factors` (#16221)

astrainfinita committed 3 years ago

20f94541

feat(field_theory/normal): Define the normal closure (#16144)

tb65536 committed 3 years ago

17ab30b2

chore(analysis/special_functions): correct typo (#16280)

mcdoll committed 3 years ago

e6c6dfd5

feat(*): replace fact(0 < t) with ne_zero (#16145)

ericrbg committed 3 years ago

879155bf

feat(analysis/normed_space/star/basic): add `cstar_ring` instances for `pi` and `prod` (#16254)

j-loreaux committed 3 years ago

b490ab4a

feat(analysis/seminorm): Add construction of seminorm over normed fields (#15893)

mcdoll committed 3 years ago

d032ed1d

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721)

faenuccio committed 3 years ago

7e20c8fc

remove pred lemmas

kex-y committed 3 years ago

b7571ff2

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/bc

kex-y committed 3 years ago

2bcaaeeb

chore(set_theory/cardinal/ordinal): follow your linter (#16265)

adomani committed 3 years ago

1b8a0c29

chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)

YaelDillies committed 3 years ago

daec7d61

feat(order/heyting/regular): Heyting-regular elements (#16033)

YaelDillies committed 3 years ago

24b08ce6

feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277)

adomani committed 3 years ago

e4b9af26

feat(data/nat/factorization/basic): lemmas about `n.factorization p = 0` (#16185)

stuart-presnell committed 3 years ago

8ad70779

feat(linear_algebra/affine_space/affine_subspace): `map_eq_bot_iff` (#16285)

jsm28 committed 3 years ago

211bf1ab

Newer Older