leanprover-community/mathlib3

Pull Requests Commits

golf and cleanup

jcommelin committed 3 years ago

4a1dd913

simplified thanks to sgouezel

loefflerd committed 3 years ago

c8ea1e9e

docstring fixes

loefflerd committed 3 years ago

14f3f475

feat(measure_theory/integral): cts fcns on [0,\infty) with exponential decay are integrable

loefflerd committed 3 years ago

124252bb

chore(linear_algebra/alternating): golf using injective APIs (#12536)

eric-wieser committed 3 years ago

5d405e2a

chore(algebra/module/linear_map): golf using injective APIs (#12535)

eric-wieser committed 3 years ago

bc9dda83

chore(data/{finsupp,dfinsupp}/basic): use the injective APIs (#12534)

eric-wieser committed 3 years ago

94e9bb55

chore(real/cau_seq_completion): put class in Prop (#12533)

PatrickMassot committed 3 years ago

b8d176e0

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

leanprover-community-bot committed 3 years ago

1f6a2e9d

feat(data/equiv/basic): lemmas about composition with equivalences (#10693)

antoinelab01 committed 3 years ago

2a3ecad0

chore(order/well_founded_set): golf two proofs (#12529)

eric-wieser committed 3 years ago

d69cda1e

feat(set_theory/cardinal_ordinal): `#(list α) ≤ max ω (#α)` (#12519)

vihdzp committed 3 years ago

709a3b70

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

Older