leanprover-community/mathlib3

Pull Requests Commits

feat(topology/vector_bundle): direct sum of topological vector bundles (#12512)

hrmacbeth committed 3 years ago

feb24fb6

feat(category_theory): cases in which (co)equalizers are split monos (epis) (#12498)

javra committed 3 years ago

1d67b07c

feat(algebra/order/hom/ring): Ordered ring isomorphisms (#12158)

YaelDillies committed 3 years ago

b4572d16

feat(data/finset/noncomm_prod): add noncomm_prod_commute (#12521)

nomeata committed 3 years ago

4ad5c5a3

feat(group_theory/subgroup/basic): disjoint_iff_mul_eq_one (#12505)

nomeata committed 3 years ago

fac5ffed

feat(set_theory/ordinal_arithmetic): prove `enum_ord_le_of_subset` (#12199)

vihdzp committed 3 years ago

1597e9a2

feat(data/finset/noncomm_prod): add noncomm_prod_congr (#12520)

nomeata committed 3 years ago

ab6a892b

feat(ring_theory/polynomial/eisenstein): add cyclotomic_comp_X_add_one_is_eisenstein_at (#12447)

riccardobrasca committed 3 years ago

c0ba4d69

chore(algebra/*): move some lemmas about is_unit from associated.lean (#12526)

Ruben-VandeVelde committed 3 years ago

94cbfad7

feat(data/int/gcd): add gcd_pos_iff (#12522)

Ruben-VandeVelde committed 3 years ago

9c13d629

feat(set_theory/ordinal_arithmetic): `brange_const` (#12483)

vihdzp committed 3 years ago

6dd32492

refactor(algebra/group/inj_surj): add npow and zpow to all definitions (#12126)

eric-wieser committed 3 years ago

07980376

chore(field_theory/laurent): drop unused 'have'. (#12516)

Ruben-VandeVelde committed 3 years ago

b4a7ad6c

chore(combinatorics/configuration): don't use classical.some in a proof (#12515)

Ruben-VandeVelde committed 3 years ago

dc093e91

feat(set_theory/cardinal): `sum_le_sup_lift` (#12513)

vihdzp committed 3 years ago

ffa6e6d6

fix(ring_theory/ideal/operations): fix a name and dot notation (#12507)

alreadydone committed 3 years ago

43cb3ffc

feat(measure_theory/measure/finite_measure_weak_convergence): generalize scalar action (#12503)

eric-wieser committed 3 years ago

b2377ea2

doc(order/succ_pred/basic): fix typo (#12501)

meithecatte committed 3 years ago

65095fe1

feat(algebra/group/to_additive): add to_additive doc string linter (#12487)

nomeata committed 3 years ago

47182da5

chore(set_theory/game/nim): General golfing (#12471)

vihdzp committed 3 years ago

ccdcce13

feat(algebra/homology/homotopy) : `mk_coinductive` (#12457)

jjaassoonn committed 3 years ago

b3fba033

feat(analysis/normed_space): allow non-unital C^* rings (#12327)

kim-em committed 3 years ago

14997d0e

chore(counterexamples/canonically_ordered_comm_semiring_two_mul): golf (#12504)

eric-wieser committed 3 years ago

74746bde

chore(*): move `has_scalar` instances before `add_comm_monoid` instances (#12502)

eric-wieser committed 3 years ago

5f6d30ec

feat(measure_theory/integral/periodic.lean): add lemma `function.periodic.tendsto_at_bot_interval_integral_of_pos'` (#12500)

ocfnash committed 3 years ago

e409a904

feat(ring_theory/coprime/basic): lemmas about multiplying by units (#12480)

Ruben-VandeVelde committed 3 years ago

390554d2

chore(number_theory/number_field): golf `int.not_is_field` (#12451)

Aresh-P committed 3 years ago

9728bd25

feat(algebra/associated): add pow_not_prime (#12493)

Ruben-VandeVelde committed 3 years ago

1b4ee53b

feat(measure_theory/function/uniform_integrable): Uniform integrability and Vitali convergence theorem (#12408)

kex-y committed 3 years ago

f28023e9

feat(probability_theory/stopping): define progressively measurable processes (#11350)

kex-y committed 3 years ago

1ee91a5c

Newer Older