leanprover-community/mathlib

Pull Requests Commits

sgouezel committed 3 years ago

35e4f2d3

chore(*): use `*_*_*_comm` where possible (#12372)

eric-wieser committed 3 years ago

3007f24c

feat(field_theory/krull_topology): added krull_topology_t2 (#11973)

Sebastian-Monnet committed 3 years ago

3fb051dc

chore(data/polynomial/monic): remove useless lemma (#12364)

ericrbg committed 3 years ago

5a56e464

chore(category_theory/idempotents) replaced "idempotence" by "idem" (#12362)

joelriou committed 3 years ago

a4e936ca

sgouezel committed 3 years ago

25437fbb

feat(linear_algebra): generalize `linear_equiv.finrank_eq` to rings (#12358)

Vierkantor committed 3 years ago

1f39ada7

feat(measure_theory/function/locally_integrable): define locally integrable (#12216)

fpvandoorn committed 3 years ago

c223a81b

feat(order/category/CompleteLattice): The category of complete lattices (#12348)

YaelDillies committed 3 years ago

cd98967d

feat(category_theory/idempotents): biproducts in idempotent completions (#12333)

joelriou committed 3 years ago

37885e8c

refactor(category_theory/functor): a folder for concepts directly related to functors (#12346)

TwoFX committed 3 years ago

73dd4b54

feat(data/finsupp/basic): Version of `finsupp.prod_add_index` with weaker premises (#11353)

stuart-presnell committed 3 years ago

456898c7

refactor(group_theory/general_commutator): Rename `general_commutator` to `subgroup.commutator` (#12308)

tb65536 committed 3 years ago

1447c401

chore(algebra): move star_ring structure on free_algebra (#12297)

kim-em committed 3 years ago

92cbcc32

feat(algebra/monoid_algebra/basic): add monomial_hom (#12283)

todbeibrot committed 3 years ago

9c71c0f0

feat(algebra/{group/with_one,order/monoid}): equivs for `with_zero` and `with_one` (#12275)

eric-wieser committed 3 years ago

c7498d08

doc(algebra,data/fun_like): small morphism documentation improvements (#11642)

Vierkantor committed 3 years ago

474aecb9

feat(ring_theory/dedekind_domain/ideal): add height_one_spectrum (#12244)

mariainesdff committed 3 years ago

33c0a1cb

feat(algebra/algebra,data/equiv/ring): `{ring,alg}_equiv.Pi_congr_right` (#12289)

Vierkantor committed 3 years ago

200c2541

feat(ring_theory/polynomial/eisenstein): add a technical lemma (#11839)

riccardobrasca committed 3 years ago

e700d561

feat(measure_theory/function/convergence_in_measure): Define convergence in measure (#11774)

kex-y committed 3 years ago

770a7ce2

feat(archive/100-theorems-list): Partition theorem (#4259)

b-mehta committed 3 years ago

b25bad7d

chore(measure_theory/function/strongly_measurable): remove useless no_zero_divisors assumption (#12353)

sgouezel committed 3 years ago

dc72624e

feat(measure_theory/group): add measures invariant under inversion/negation (#11954)

fpvandoorn committed 3 years ago

58c20c19

feat(group_theory/subgroup/basic): Centralizer subgroup (#11946)

tb65536 committed 3 years ago

f3a04eda

doc(data/set_like/basic): tidy up docstring (#12337)

kbuzzard committed 3 years ago

2f86b497

chore(linear_algebra/basic): make `linear_map.id_coe` elegible for `dsimp` (#12334)

eric-wieser committed 3 years ago

dfacfd34

refactor(group_theory/solvable): Delete duplicate lemma (#12307)

tb65536 committed 3 years ago

f322fa0f

feat(analysis/complex): maximum modulus principle (#12050)

urkud committed 3 years ago

7f52f94a

feat(analysis/complex/liouville): prove Liouville's theorem (#12095)

urkud committed 3 years ago

b5faa34b

Newer Older