leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/lie/basic): define ideal operations for Lie modules (#5337)

Oliver Nash committed 5 years ago

dc719a9d

feat(field_theory/intermediate_field): lift2_alg_equiv (#5344)

tb65536 committed 5 years ago

a649c59a

feat(algebra/algebra/basic): arrow_congr for alg_equiv (#5346)

tb65536 committed 5 years ago

4415dc0e

chore(linear_algebra/{multilinear,alternating}): Generalize smul and neg instance (#5364)

eric-wieser committed 5 years ago

07b5618a

feat(field_theory.minimal_polynomial): add results for GCD domains (#5336)

riccardobrasca committed 5 years ago

b1c56b1b

feat(topology/subset_properties): add instances for totally_disconnected_spaces (#5334)

callesonne committed 5 years ago

f443792f

feat(tactic/induction): add induction'/cases'/eliminate_hyp/eliminate_expr tactics (#5027)

JLimperg committed 5 years ago

d36af184

feat(data/equiv): Add `congr_arg`, `congr_fun`, and `ext_iff` lemmas to equivs (#5367)

eric-wieser committed 5 years ago

a65de994

feat(field_theory/splitting_field): add splits_X theorem (#5343)

tb65536 committed 5 years ago

dad88d8c

chore(field_theory/adjoin): move dim/findim lemmas (#5342)

tb65536 committed 5 years ago

cf7377ac

chore(order/filter/at_top_bot): add/rename lemmas about limits like `±∞*c` (#5333)

urkud committed 5 years ago

0d7ddf1f

feat(analysis/mean_inequalities): add weighted generalized mean inequality for ennreal (#5316)

RemyDegenne committed 5 years ago

1d37ff18

feat(group_theory/congruence): Add inv and neg (#5304)

eric-wieser committed 5 years ago

cecab59d

feat(computability/language): define formal languages (#5291)

foxthomson committed 5 years ago

6dc50004

feat(algebra/direct_sum): constructor for morphisms into direct sums (#5204)

jcommelin committed 5 years ago

67b5ff6f

feat (topology/instances/ennreal): summability from finite sum control (#5363)

sgouezel committed 5 years ago

c722b967

chore(analysis/normed_space/ordered): minor golfing (#5356)

urkud committed 5 years ago

91e5b8a7

feat(measurable_space): infix notation for measurable_equiv (#5329)

fpvandoorn committed 5 years ago

2245cfb6

chore(analysis/calculus/*): rename `*.of_local_homeomorph` to `local_homeomorph.*_symm` (#5358)

urkud committed 5 years ago

6f69741b

feat(category_theory/adjunction): adjoint lifting theorems (#5118)

b-mehta committed 5 years ago

714bc15f

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

leanprover-community-bot committed 5 years ago

b7a9615a

chore(analysis/calculus): move the definition of `formal_multilinear_series` to a new file (#5348)

urkud committed 5 years ago

88fb7cab

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

leanprover-community-bot committed 5 years ago

36eec1a9

feat(category_theory/sites): naming and attributes (#5340)

b-mehta committed 5 years ago

eb9164bd

feat(field_theory/galois): Is_galois iff is_galois top (#5285)

tb65536 committed 5 years ago

68818b3a

feat(ring_theory/finiteness): add iff_quotient_mv_polynomial (#5321)

riccardobrasca committed 5 years ago

5ced4dde

chore(*): generalize some lemmas from `linear_ordered_semiring` to `ordered_semiring` (#5327)

urkud committed 5 years ago

3afdf41f

refactor(ring_theory/polynomial/homogeneous): redefine `mv_polynomial.homogeneous_component` (#5294)

urkud committed 5 years ago

dad5aabe

feat(group_theory/perm/subgroup): Add some simple subgroups of permutations (#5279)

eric-wieser committed 5 years ago

9cc8835b

feat(category_theory/sites): sheaves on types (#5259)

kckennylau committed 5 years ago

84f99388

Newer Older