Commits leanprover-community/mathlib3

feat(combinatorics/hall): Hall's marriage theorem (#5695)

agusakov committed 4 years ago

72141fdc

feat(data/set/finite): fintype_of_univ_finite (#6164)

jcommelin committed 4 years ago

db305fb5

feat(data/real/irrational): define Liouville numbers (#6158)

adomani committed 4 years ago

2f566202

chore(group_theory/perm, linear_algebra/alternating): add some helper lemmas for gh-5269 (#6186)

eric-wieser committed 4 years ago

64914d36

chore(topology/homeomorph): review, add `prod_punit`/`punit_prod` (#6180)

urkud committed 4 years ago

cee5ddf3

feat(data/nat/bitwise): test bits of powers of two (#6070)

b-mehta committed 4 years ago

6c602c7e

refactor(algebra/lie/of_associative): remove `ring_commutator` namespace; use `ring` instead (#6181)

ocfnash committed 4 years ago

1ad29d69

refactor(algebra/lie/*): rename `lie_algebra.morphism` --> `lie_hom`, `lie_algebra.equiv` --> `lie_equiv` (#6179)

ocfnash committed 4 years ago

abf72e6d

doc(algebra/field): added module doc (#6177)

Julian-Kuelshammer committed 4 years ago

b3347e56

feat(algebra/lie/submodule): Lie submodules form a modular lattice (#6176)

ocfnash committed 4 years ago

af8b60b8

feat(algebra/ordered_ring): a product is at least one if both factors are (#6172)

adomani committed 4 years ago

b9354dda

feat(group_theory/subgroup): prove relation between pointwise product of submonoids/subgroups and their join (#6165)

AdrianDoM committed 4 years ago

194ec667

feat(field_theory/polynomial_galois_group): Restriction from splitting field of composition (#6148)

tb65536 committed 4 years ago

f151da2a

feat(order/well_founded_set) : Define when a set is well-founded with `set.is_wf` (#6113)

awainverse committed 4 years ago

7b4a9e5f

feat(data/complex): order structure (#4684)

kim-em committed 4 years ago

a557f8bd

doc(analysis/analytic/inverse): fix mathjax output (#6175)

sgouezel committed 4 years ago

39090c8c

feat(topology/order): discrete_topology_bot (#6163)

jcommelin committed 4 years ago

58632ac6

feat(linear_algebra/matrix): generalize some `is_basis.to_matrix` results (#6127)

Vierkantor committed 4 years ago

fdace951

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

leanprover-community-bot committed 4 years ago

d405c5e9

refactor(topology/subset_properties.lean): split the subset_properties.lean file (#6161)

callesonne committed 4 years ago

59daf530

refactor(algebra/lie/basic): split giant file into pieces (#6141)

ocfnash committed 4 years ago

97a56e63

doc(algebra/euclidean_domain): module doc (#6107)

Julian-Kuelshammer committed 4 years ago

97f89af6

chore(field_theory,ring_theory): reduce dependencies of `power_basis.lean` (#6104)

Vierkantor committed 4 years ago

906e03de

feat(data/finset/lattice): `inf` and `sup` on complete_linear_orders produce an element of the set (#6103)

eric-wieser committed 4 years ago

330129d4

perf(ring_theory/{noetherian,ideal/basic}): Simplify proofs of Krull's theorem and related theorems (#6082)

cemulate committed 4 years ago

3959a8bb

feat(order/compactly_generated): A compactly-generated modular lattice is complemented iff atomistic (#6071)

awainverse committed 4 years ago

030107f6

feat(ring_theory/polynomial/chebyshev/dickson): Introduce generalised Dickson polynomials (#5869)

Julian-Kuelshammer committed 4 years ago

7fb7fb36

feat(analysis/analytic/inverse): convergence of the inverse of a power series (#5854)

sgouezel committed 4 years ago

c70feebd

feat(algebra/subalgebra): Trivial subalgebra has trivial automorphism group (#5672)

tb65536 committed 4 years ago

19f24ced

feat(archive/imo): formalize 1987Q1 (#4731)

urkud committed 4 years ago

983cb905