leanprover-community/mathlib

Pull Requests Commits

Merge branch 'group-hom-simp' into eval-PRd

urkud committed 5 years ago

575a55e2

Merge branch 'linft-nc-smul' into eval-PRd

urkud committed 5 years ago

941c88ba

Merge branch 'degree-gi' into eval-PRd

urkud committed 5 years ago

ea59a49b

feat(algebra/big_operators/nat_antidiagonal): a few more lemmas

urkud committed 5 years ago

daa53e9b

feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)`

urkud committed 5 years ago

b42c9144

urkud committed 5 years ago

f5436e41

chore(algebra/group/hom): use `coe_comp` in `simp` lemmas

urkud committed 5 years ago

c6842072

chore(order/galois_connection): define `with_bot.gi_get_or_else_bot`

urkud committed 5 years ago

4c1eb2f6

Merge branch 'master' into bundled-eval

urkud committed 5 years ago

709f8344

urkud committed 5 years ago

131c9356

urkud committed 5 years ago

318d50a5

feat(analysis/normed_space/add_torsor): continuity of `vadd`/`vsub` (#4751)

urkud committed 5 years ago

a9d3ce8e

fix(tactic/core): fix infinite loop in emit_code_here (#4746)

digama0 committed 5 years ago

e7a4b12c

chore(linear_algebra/tensor_product): missing simp lemmas (#4769)

jcommelin committed 5 years ago

151f0dd2

chore(ring_theory/unique_factorization_domain): fix some lemma names (#4765)

awainverse committed 5 years ago

69f550cb

chore(algebra/group/pi): add `pi.has_div` (#4776)

urkud committed 5 years ago

14cff9ac

Merge branch 'polylemmas' into bundled-eval

urkud committed 5 years ago

bee93eea

urkud committed 5 years ago

7532c6e5

Merge branch 'master' into polylemmas

urkud committed 5 years ago

1fc2f55c

Golf 1 more proof

urkud committed 5 years ago

53b60da1

urkud committed 5 years ago

82ac1be5

chore(analysis/normed_space): add 2 `@[simp]` attrs (#4775)

urkud committed 5 years ago

f056468f

chore(data/polynomial/eval): remove commutativity in map_sum and map_neg

riccardobrasca committed 5 years ago

b508ed98

chore(data/polynomial/degree/basic): add supp_card_le_succ_nat_degree

riccardobrasca committed 5 years ago

eece34a2

feat(algebra/direct_sum): Fix two todos about generalizing over unique types (#4764)

eric-wieser committed 5 years ago

cae77dc7

feat(ring_theory/polynomial/content): `gcd_monoid` instance on polynomials over gcd domain (#4760)

awainverse committed 5 years ago

de6a9d41

feat(data/polynomial/ring_division): Two easy lemmas about polynomials (#4742)

riccardobrasca committed 5 years ago

570c293a

feat(linear_algebra/nonsingular_inverse): add stronger form of Cramer's rule (#4737)

Oliver Nash committed 5 years ago

b9a94d69

fix(tactic/core): use eval_pexpr in run_parser_cmd (#4761)

digama0 committed 5 years ago

2987a496

feat(data/pnat/basic): Add strong induction on pnat (#4736)

riccardobrasca committed 5 years ago

8255507e

Newer Older