leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/category/BoolRing): The category of Boolean rings (#12905)

YaelDillies committed 3 years ago

2891e1be

feat(model_theory/fraisse): Construct Fraïssé limits (#12138)

awainverse committed 3 years ago

f53b2399

feat(combinatorics/simple_graph/density): Edge density (#12431)

YaelDillies committed 3 years ago

6ac7c18d

feat(algebra/module/torsion): define torsion submodules (#12027)

pbazin committed 3 years ago

7302e116

chore(order/zorn): Review (#12175)

YaelDillies committed 3 years ago

c7745b3b

feat(topology/algebra/group): define `has_continuous_inv` and `has_continuous_neg` type classes (#12748)

j-loreaux committed 3 years ago

7c48d65c

feat(ring_theory/polynomial): mv_polynomial over UFD is UFD (#12866)

alreadydone committed 3 years ago

eabc6192

feat(*): facts about degrees/multiplicites of derivatives (#12856)

ericrbg committed 3 years ago

db760640

chore(data/polynomial/*): delete, rename and move lemmas (#12852)

astrainfinita committed 3 years ago

355645e3

feat(algebra/associated): generalize nat.prime_mul_iff (#12850)

Ruben-VandeVelde committed 3 years ago

c1fb0ed9

feat(data/list/basic): nth_le+filter lemmas (#12836)

ericrbg committed 3 years ago

a5a0d233

feat(model_theory/*): Facts about countability of first-order structures (#12819)

awainverse committed 3 years ago

892e6113

feat(number_theory/arithmetic_function): The moebius function is multiplicative (#12796)

khwilson committed 3 years ago

e6c6f006

chore(fintype/card_embedding): generalize instances (#12775)

ericrbg committed 3 years ago

0faebd2a

feat(number_theory/function_field): add completion with respect to place at infinity (#12715)

mariainesdff committed 3 years ago

04274301

feat(topology/nhds_set): add `has_basis_nhds_set` (#12908)

urkud committed 3 years ago

ca93096b

feat(measure_theory/integral): continuous functions with exponential decay are integrable (#12539)

loefflerd committed 3 years ago

399ce38e

feat(ring_theory/principal_ideal_domain): add some irreducible lemmas (#12903)

Ruben-VandeVelde committed 3 years ago

df348164

refactor(category_theory/abelian): trivial generalisations (#12897)

kim-em committed 3 years ago

a9781152

chore(topology/separation): move a lemma, golf (#12896)

urkud committed 3 years ago

d4e27d0b

feat(topology/continuous_function/bounded): add `bounded_continuous_function.tendsto_iff_tendsto_uniformly` (#12894)

j-loreaux committed 3 years ago

e968b6d1

chore(data/set/intervals): golf, rename (#12893)

urkud committed 3 years ago

a370cf05

feat(topology/separation): generalize tendsto_const_nhds_iff to t1_space (#12883)

fpvandoorn committed 3 years ago

5ef365a3

docs(data/set/pairwise): Explain preference for `s.pairwise_disjoint id` (#12878)

YaelDillies committed 3 years ago

6696bdd9

feat(data/complex/is_R_or_C): generalize `is_R_or_C.proper_space_span_singleton` to all finite dimensional submodules (#12877)

eric-wieser committed 3 years ago

30449be1

feat(tactic/ext): support rintro patterns in `ext` (#12875)

digama0 committed 3 years ago

debdd909

chore(data/int/basic): remove some `eq.mpr`s from `int.induction_on'` (#12873)

eric-wieser committed 3 years ago

8e50164d

fix(ring_theory/algebraic): Make `is_transcendental_of_subsingleton` fully general (#12870)

vihdzp committed 3 years ago

ae695782

feat(data/{nat, real}/sqrt): Some simple facts about square roots (#12851)

khwilson committed 3 years ago

706a824c

feat(group_theory/order_of_element): finite orderness is closed under mul (#12750)

Julian committed 3 years ago

ec434b75

Newer Older