leanprover-community/mathlib3

Pull Requests Commits

fix `field_theory/galois`

j-loreaux committed 3 years ago

Verified 8fe5523f

j-loreaux committed 3 years ago

4a80b8a1

j-loreaux committed 3 years ago

bbe8d566

j-loreaux committed 3 years ago

16da58f7

try lowering instance priority

j-loreaux committed 3 years ago

Verified edd1f94f

j-loreaux committed 3 years ago

Verified 27dad871

j-loreaux committed 3 years ago

Verified aad1c343

j-loreaux committed 3 years ago

e1c747f4

j-loreaux committed 3 years ago

c413a46b

fix algebra/algebra/subalgebra/basic

j-loreaux committed 3 years ago

811f1862

fix ring_theory/ideal/operations

j-loreaux committed 3 years ago

3a2a76d0

fix to_direct_sum

j-loreaux committed 3 years ago

193c6748

fix data/matrix/basic

j-loreaux committed 3 years ago

da9d9d7f

fix algebra/monoid_algebra/basic

j-loreaux committed 3 years ago

156aa4a9

fix ring_theory/localization/basic

j-loreaux committed 3 years ago

4b5ed67d

add convenience lemma

j-loreaux committed 3 years ago

15ec2064

j-loreaux committed 3 years ago

Verified ed4aab9d

finish algebra/algebra/basic

j-loreaux committed 3 years ago

Verified bd6ae844

j-loreaux committed 3 years ago

Verified a176438c

feat(data/polynomial/eval): add polynomial.map_bit0/1 (#16481)

alexjbest committed 3 years ago

d268bb7a

feat(topology/algebra/uniform_group): the quotient of a first countable complete topological group by a normal subgroup is itself complete (#16368)

j-loreaux committed 3 years ago

c0ad3bf9

feat(convex/specific_functions): specific case of Jensen's inequality for powers (#16186)

dtumad committed 3 years ago

01a8a9f8

feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum (#15821)

ADedecker committed 3 years ago

3c93c656

feat(data/sym/basic): add `fill` `filter_ne` and `sigma_ext` (#16316)

pimotte committed 3 years ago

a945b376

feat(topology/algebra/order/intermediate_value): intervals are connected (#16473)

jsm28 committed 3 years ago

c64fb26a

feat(analysis/normed_space/units): maximal ideals in complete normed rings are closed (#16303)

j-loreaux committed 3 years ago

4ff10212

chore(ring_theory/local_properties): remove coercions from `ring_hom` to `monoid_hom` (#16453)

eric-wieser committed 3 years ago

5bd4f627

feat(data/complex/module): define `real_part` and `imaginary_part` (#16438)

j-loreaux committed 3 years ago

06ae0493

feat(ring_theory/dedekind_domain/ideal): construct map between the sets of prime factors of ideal `I` and `J` induced by an isomorphism between `R/I` and `S/J` (#16455)

Paul-Lez committed 3 years ago

36e01301

feat(data/nat/{choose/multinomial,factorial/big_operations}): add multinomial coefficient definition with basic lemma's (#16170)

pimotte committed 3 years ago

a280c1e5

Older