leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into fin_range

YaelDillies committed 4 years ago

989923d6

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

feat(analysis/normed_space/add_torsor_bases): the convex hull has non-empty interior iff the affine span is top (#9727)

ocfnash committed 4 years ago

39db98c8

chore(field_theory/galois): speedup a slow convert (#9782)

kim-em committed 4 years ago

2e62b33c

feat(linear_algebra/affine_space/independent): affine equivalences preserve affine independence of sets of points (#9776)

ocfnash committed 4 years ago

27d28a84

feat(topology/metric_space): closed if spaced out (#9754)

urkud committed 4 years ago

fb5c0bec

split(data/list/permutation): split off `data.list.basic` (#9749)

YaelDillies committed 4 years ago

6cd6ff44

Older