leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/integral_domain): finite domains are division rings (#9823)

jcommelin committed 4 years ago

8366f932

chore(group_theory/submonoid/center): add decidable_mem_center (#9825)

eric-wieser committed 4 years ago

4ebeb055

feat(group_theory/index): Index of top and bottom subgroups (#9819)

tb65536 committed 4 years ago

3d00081c

refactor(algebra/order/sub): rename sub -> tsub (#9793)

fpvandoorn committed 4 years ago

68a674ef

feat(field_theory/finite/galois_field): uniqueness of finite fields (#9817)

AaronGreen001 committed 4 years ago

5223e262

fix(algebra/module/submodule_lattice): correct bad lemma (#9809)

eric-wieser committed 4 years ago

49ab444f

feat(linear_algebra/free_module/rank): rank of free modules (#9810)

riccardobrasca committed 4 years ago

24901dde

refactor(*): replace comm_ring/integral_domain with ring/domain where possible (#9739)

kim-em committed 4 years ago

2f548407

chore(set_theory/cardinal): add `map`, `induction_on` etc (#9812)

urkud committed 4 years ago

a6d5ba81

feat(group_theory/subgroup/basic): `subgroup_of_self` (#9818)

tb65536 committed 4 years ago

9dafdf79

feat(analysis/complex/basic): a complex-valued function `has_sum` iff its real part and imaginary part `has_sum` (#9648)

kex-y committed 4 years ago

68987280

chore(*): remove uses of `universe variable` (#9794)

digama0 committed 4 years ago

cd343474

feat(group_theory/index): Relative index (#9780)

tb65536 committed 4 years ago

2d17c5a2

refactor(*): rename some declarations ending with '' (#9504)

kim-em committed 4 years ago

72cb2e82

fix(data/int/basic): ensure the additive group structure on integers is computable (#9803)

eric-wieser committed 4 years ago

65eef746

fix(topology/sheaves/*): Fix docstrings (#9807)

justus-springer committed 4 years ago

e61584d5

feat(ring_theory/dedekind_domain): connect (/) and (⁻¹) on fractional ideals (#9808)

Vierkantor committed 4 years ago

34aa23af

refactor(analysis/inner_product_space/projection): speedup proof (#9804)

kim-em committed 4 years ago

065a7081

feat(topology/connected): product of connected spaces is a connected space (#9789)

urkud committed 4 years ago

b961b684

refactor(algebra/domain): make domain and integral_domain mixins (#9719)

kim-em committed 4 years ago

ff3e868c

feat(algebra/big_operators/order): Upper bound on the cardinality of `finset.bUnion` (#9797)

YaelDillies committed 4 years ago

a7bc7174

feat(data/nat/modeq): Upper bound for `chinese_remainder` (#9783)

tb65536 committed 4 years ago

4df649cb

feat(data/nat/succ_pred): `ℕ` is succ- and pred- archimedean (#9730)

YaelDillies committed 4 years ago

1f8c96ba

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

leanprover-community-bot committed 4 years ago

1ec385df

feat(analysis/box_integral): Divergence thm for a Henstock-style integral (#9496)

urkud committed 4 years ago

04094c4b

refactor(ring_theory/adjoin/fg): replace a fragile convert with rewrites (#9786)

kim-em committed 4 years ago

5eee6a27

refactor(algebra/order): replace typeclasses with constructors (#9725)

kim-em committed 4 years ago

98d07d31

feat(tactic/to_additive): Improvements to to_additive (#5487)

alexjbest committed 4 years ago

442382db

feat(tactic/lint): improve check_univs linter (#9698)

fpvandoorn committed 4 years ago

8b7e16fe

refactor(ring_theory/ideal/operations): generalize various definitions to remove negation and commutativity (#9737)

eric-wieser committed 4 years ago

b112d4dd

Older