leanprover-community/mathlib3

Pull Requests Commits

chore(logic/function/basic): add function.ne_iff (#12288)

eric-wieser committed 3 years ago

9f721bab

feat(algebra/algebra/operations): `submodule.map_pow` and opposite lemmas (#12374)

eric-wieser committed 3 years ago

9deeddb3

chore(algebra/ring/basic): generalize lemmas to non-associative rings (#12411)

eric-wieser committed 3 years ago

6f74d3cc

sgouezel committed 3 years ago

f7476a2e

refactor(analysis/normed_space/basic): split into normed_space and ../normed/normed_field (#12410)

mcdoll committed 3 years ago

ce26d75d

chore(probability/independence): change to set notation and `measurable_set` (#12400)

kex-y committed 3 years ago

423328e0

feat(algebra/module/submodule_pointwise): pointwise negation (#12405)

eric-wieser committed 3 years ago

a283e17b

chore(measure_theory/function/egorov): rename `uniform_integrability` file to `egorov` (#12402)

kex-y committed 3 years ago

90e2957e

feat(linear_algebra/matrix.determinant): add `matrix.det_neg` (#12396)

eric-wieser committed 3 years ago

7959d982

refactor(group_theory/*): Rename `general_commutator.lean` to `commutator.lean` (#12388)

tb65536 committed 3 years ago

c96fb62b

feat(algebra/big_operators/basic): prod_dvd_prod_of_subset (#12383)

ericrbg committed 3 years ago

d00cbee3

feat(ring_theory/ideal): `map f (I^n) = (map f I)^n` (#12370)

Vierkantor committed 3 years ago

22ddf9a3

feat(ring_theory/unique_factorization_domain): factors of `p^k` (#12369)

Vierkantor committed 3 years ago

4e8d8f27

chore(algebra/big_operators): generalize `map_prod` to `monoid_hom_class` (#12354)

Vierkantor committed 3 years ago

f191f521

chore(ring_theory/localization): `localization_map_bijective` rename & `field` instance version (#12375)

ericrbg committed 3 years ago

20d95410

feat(probability): define conditional probability and add basic related theorems (#12344)

rish987 committed 3 years ago

35086a11

perf(data/fintype/basic): speed up mem_of_mem_perms_of_list (#12389)

digama0 committed 3 years ago

1eebec51

doc(*): fix broken markdown links (#12385)

eric-wieser committed 3 years ago

9daa2338

feat(algebra/ring): add non-unital and non-associative rings (#12300)

kim-em committed 3 years ago

b77ff234

feat(set_theory/principal): prove theorems about additive principal ordinals (#11704)

vihdzp committed 3 years ago

fefe359d

feat(algebra/divisibility): generalise basic facts to semigroups (#12325)

kim-em committed 3 years ago

a9902d54

feat(algebra/star): replace star_monoid with star_semigroup (#12299)

kim-em committed 3 years ago

cc9de07a

feat(algebra/euclidean_domain,data/int/basic): dvd_div_of_mul_dvd (#12382)

ericrbg committed 3 years ago

4ba9098e

feat(topology/bornology/basic): Define bornology (#12036)

j-loreaux committed 3 years ago

269280a1

chore(topology/algebra/valuation): add universe (#11962)

mariainesdff committed 3 years ago

5c2fa35a

feat(ring_theory/integral_domain): finite integral domain is a field (#12376)

ericrbg committed 3 years ago

818c81fc

chore(algebra/group/prod): `prod.swap` commutes with arithmetic (#12367)

eric-wieser committed 3 years ago

130e07d3

feat(category_theory/abelian/homology): Adds API for homology mimicking that of (co)kernels. (#12171)

adamtopaz committed 3 years ago

5e36e121

feat(algebra/algebra/spectrum, analysis/normed_space/spectrum): prove the spectrum of any element in a complex Banach algebra is nonempty (#12115)

j-loreaux committed 3 years ago

b45657ff

feat(combinatorics/set_family/lym): Lubell-Yamamoto-Meshalkin inequalities (#11248)

YaelDillies committed 3 years ago

29c84f71

Newer Older