leanprover-community/mathlib3

Pull Requests Commits

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

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

feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971)

awainverse committed 5 years ago

cbd67cf4

feat(linear_algebra/free_algebra): Show that free_monoid forms a basis over free_algebra (#5868)

eric-wieser committed 5 years ago

5f328b6e

feat(data/nat/factorial): additional inequalities (#6026)

adomani committed 5 years ago

36b35107

feat(data/real/sqrt): added some missing sqrt lemmas (#5933)

benjamindavidson committed 5 years ago

360fa07e

Newer Older