leanprover-community/mathlib

Pull Requests Commits

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

remove redundant lemma

dupuisf committed 4 years ago

df42a2f6

Update src/data/complex/is_R_or_C.lean

dupuisf committed 4 years ago

Verified 35ac2507

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

fpvandoorn committed 4 years ago

8b7e16fe

conj_to_ring_equiv -> abbreviation for star_ring_equiv

dupuisf committed 4 years ago

233433b0

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

eric-wieser committed 4 years ago

b112d4dd

feat(analysis/normed/group/SemiNormedGroup/completion): add SemiNormedGroup.Completion (#9788)

riccardobrasca committed 4 years ago

71c203a9

refactor(algebra/floor): Add `ceil` as a field of `floor_ring` (#9591)

YaelDillies committed 4 years ago

80071d45

refactor(ring_theory/finiteness): replace fragile convert with rewrites (#9787)

kim-em committed 4 years ago

5ea384e8

Newer Older