leanprover-community/mathlib3

Pull Requests Commits

chore(algebra/algebra/basic): show that the ℚ-algebra structure is unique (#5980)

eric-wieser committed 5 years ago

392ebecd

feat(field_theory/polynomial_galois_group): Restriction is surjective (#5961)

tb65536 committed 5 years ago

915bff47

feat(order/filter): add lattice instance to order.ideal (#5937)

mguaypaq committed 5 years ago

e1db9093

feat(order/*): introduces complemented lattices (#5747)

awainverse committed 5 years ago

70269f3c

feat(algebra/group_power/basic): `pow_add_pow_le` (#6037)

benjamindavidson committed 5 years ago

53914334

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

leanprover-community-bot committed 5 years ago

5cb2865e

feat(algebra/big_operators/order): add fintype.sum_mono and fintype.sum_strict_mono (#6040)

eric-wieser committed 5 years ago

80c7ac1c

fix(tactic/congr): fix trivial congr/convert (#6011)

digama0 committed 5 years ago

a101788b

chore(data/quot): rename `lift_on_beta` to `lift_on_mk` (#5921)

eric-wieser committed 5 years ago

59cfa02f

feat(data/real/ennreal): use notation for ennreal (#6044)

fpvandoorn committed 5 years ago

b9e559b7

refactor(data/real/basic): make ℝ a structure (#6024)

gebner committed 5 years ago

7734d386

feat(topology/algebra/infinite_sum, topology/instances/ennreal): extend tsum API (#6017)

adomani committed 5 years ago

d2938225

feat(number_theory/bernoulli): Results regarding Bernoulli numbers as a generating function (#5957)

laughinggas committed 5 years ago

1ee00c89

improving can_assume_min

faenuccio committed 5 years ago

19c28fc8

refactor(real): protect real.pi (#6039)

sgouezel committed 5 years ago

49cf0be5

feat(data/list/sort): add sorted.rel_of_mem_take_of_mem_drop (#6027)

eric-wieser committed 5 years ago

1a7fb7e4

chore(data/dfinsupp): add simp lemmas about sum_add_hom, remove commutativity requirement (#5939)

eric-wieser committed 5 years ago

b98b5f6b

feat(data/equiv/basic): perm.subtype_congr (#5875)

pechersky committed 5 years ago

6d153f1b

feat(data/fintype/basic): inv of inj on deceq (#5872)

pechersky committed 5 years ago

bbf97744

feat(tactic/norm_swap): simplify numeral swaps (#5637)

pechersky committed 5 years ago

9993a504

chore(order/basic): add a lemma expanding `le` on pi types (#6023)

eric-wieser committed 5 years ago

4d26028e

chore(linear_algebra/quadratic_form): add polar_self, polar_zero_left, and polar_zero_right simp lemmas (#6003)

eric-wieser committed 5 years ago

e61db52e

feat(analysis/special_functions/trigonometric): add mistakenly omitted lemma (#6036)

benjamindavidson committed 5 years ago

1a2eb0b5

refactor(analysis/normed_space): simpler proof of `norm_sub_pow_two` (#6035)

Jesse Michael Han committed 5 years ago

16be8e39

doc(number_theory/{pell, sum_of_four_squares}): docstring to pell (#6030)

Julian-Kuelshammer committed 5 years ago

894ff7ad

refactor(analysis/asymptotics): make definitions immediately irreducible (#6021)

gebner committed 5 years ago

0aed8b1e

chore(linear_algebra/std_basis): move std_basis to a new file (#6020)

eric-wieser committed 5 years ago

97781b9a

feat(algebra/ordered_ring): weaken hypotheses for one_le_two (#6034)

b-mehta committed 5 years ago

6df15017

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

leanprover-community-bot committed 5 years ago

3309490a

feat(data/list/basic): drop_eq_nil_of_le (#6029)

pechersky committed 5 years ago

7812afa3

Newer Older