leanprover-community/mathlib3

Pull Requests Commits

jcommelin committed 4 years ago

3c7f67c2

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

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

feat(data/set/pairwise): Simple `pairwise_disjoint` lemmas (#9764)

YaelDillies committed 4 years ago

6f4aea44

chore(group_theory/order_of_element): order_of_units (#9777)

ericrbg committed 4 years ago

116e4267

feat(topology/metric_space): dimH is the supr of local dimH (#9741)

urkud committed 4 years ago

a7ac6996

feat(data/real/pointwise): Inf and Sup of `a • s` for `s : set ℝ` (#9707)

YaelDillies committed 4 years ago

06179ca9

feat(linear_algebra/dfinsupp): cardinality lemmas for `complete_lattice.independent` (#9705)

hrmacbeth committed 4 years ago

e8413250

Older