leanprover-community/mathlib3

Pull Requests Commits

Try to generalize to bimodules. This doesn't work so well.

eric-wieser committed 4 years ago

cdf451db

feat(data/finset/basic): Simple `finset.erase` lemmas (#9878)

YaelDillies committed 4 years ago

43cd79f9

feat(measure_theory/integral/set_integral): integral of a `is_R_or_C` function equals integral of real part + integral of imaginary part (#9735)

kex-y committed 4 years ago

76212e65

feat(topology): define class `[noncompact_space]` (#9839)

urkud committed 4 years ago

c4c71d2f

feat(data/polynomial): generalize and rename `polynomial.normalize_monic` (#9853)

Vierkantor committed 4 years ago

6f837a6e

refactor(data/complex/*): replace `complex.conj` and `is_R_or_C.conj` with star (#9640)

dupuisf committed 4 years ago

16a9031a

feat(algebra/group_power/lemmas): Positivity of an odd/even power (#9796)

YaelDillies committed 4 years ago

912039d7

refactor(data/real/ennreal): remove sub lemmas (#9857)

fpvandoorn committed 4 years ago

15d4e5f1

feat(linear_algebra/quotient): `S.restrict_scalars.quotient` is `S.quotient` (#9535)

Vierkantor committed 4 years ago

5b72c4ee

feat(logic/function/embedding): add `function.embedding.option_elim` (#9841)

urkud committed 4 years ago

9be82475

feat(linear_algebra/matrix/nonsingular_inverse): adjugate of a 2x2 matrix (#9830)

eric-wieser committed 4 years ago

14ec1c8e

feat(analysis/inner_product_space): define `orthogonal_family` of subspaces (#9718)

hrmacbeth committed 4 years ago

9c240b58

fix(ring_theory/subring): `inclusion` is a ring_hom! (#9849)

jcommelin committed 4 years ago

d8096aa6

chore(algebra/big_operators): avoid 'abel' tactic (#9833)

Ruben-VandeVelde committed 4 years ago

d8b0d1a9

chore(topology/algebra/ordered): move IVT to a new file (#9792)

urkud committed 4 years ago

de13786a

feat(topology/metric_space/isometry): add simps config (#9757)

urkud committed 4 years ago

d9daf541

feat(ring_theory/polynomial/cyclotomic): add cyclotomic_prime_pow_eq_geom_sum and supporting lemmas (#9845)

alexjbest committed 4 years ago

fe5ddaf4

chore(set_theory/cardinal): ensure `c ^ ↑n = c ^ n` is definitional (#9842)

urkud committed 4 years ago

edd801f7

feat(group_theory/index): Special cases of relindex (#9831)

tb65536 committed 4 years ago

777f11c8

feat(data/nat/modeq): `modeq.le_of_lt_add` (#9816)

tb65536 committed 4 years ago

bfa40102

refactor(*): remove integral_domain, rename domain to is_domain (#9748)

kim-em committed 4 years ago

da01792c

chore(*): bump to lean 3.34.0 (#9824)

kim-em committed 4 years ago

3c11bd77

feat(ring_theory/integral_domain): finite domains are division rings (#9823)

jcommelin committed 4 years ago

8366f932

chore(group_theory/submonoid/center): add decidable_mem_center (#9825)

eric-wieser committed 4 years ago

4ebeb055

feat(group_theory/index): Index of top and bottom subgroups (#9819)

tb65536 committed 4 years ago

3d00081c

refactor(algebra/order/sub): rename sub -> tsub (#9793)

fpvandoorn committed 4 years ago

68a674ef

feat(field_theory/finite/galois_field): uniqueness of finite fields (#9817)

AaronGreen001 committed 4 years ago

5223e262

fix(algebra/module/submodule_lattice): correct bad lemma (#9809)

eric-wieser committed 4 years ago

49ab444f

feat(linear_algebra/free_module/rank): rank of free modules (#9810)

riccardobrasca committed 4 years ago

24901dde

refactor(*): replace comm_ring/integral_domain with ring/domain where possible (#9739)

kim-em committed 4 years ago

2f548407

Older