leanprover-community/mathlib

Pull Requests Commits

eric-wieser committed 3 years ago

3dcf1670

eric-wieser committed 3 years ago

716b8887

eric-wieser committed 3 years ago

5f529fd4

feat(logic/lemmas): Distributivity of `if then else` (#14146)

YaelDillies committed 3 years ago

9dc9c3ea

feat(linear_algebra/multilinear/finite_dimensional): generalize to finite and free (#14199)

eric-wieser committed 3 years ago

ae6a7c3f

chore(data/multiset/basic): `∅` → `0` (#14211)

vihdzp committed 3 years ago

59facea4

chore(measure_theory/function/strongly_measurable): golf some proofs (#14209)

urkud committed 3 years ago

d08f7340

chore(data/multiset/basic): Inline instances (#14208)

vihdzp committed 3 years ago

50696a85

feat(data/polynomial/mirror): Central coefficient of `p * p.mirror` (#14096)

tb65536 committed 3 years ago

9f6f605b

feat(category_theory/limits): reindexing (co/bi)products (#14193)

kim-em committed 3 years ago

f48cbb16

feat(data/multiset/basic): `pair_comm` (#14207)

vihdzp committed 3 years ago

ca5930df

feat(analysis/special_functions/trigonometric/arctan): add `real.range_arctan` (#14204)

urkud committed 3 years ago

6b291d7b

feat(analysis/normed_space/M_structure): Define L-projections, show they form a Boolean algebra (#12173)

mans0954 committed 3 years ago

632fef37

refactor(algebra/parity): Generalize to division monoids (#14187)

YaelDillies committed 3 years ago

0afb90b4

feat(topology/instances/matrix): add topological/continuous instances (#14202)

aronerben committed 3 years ago

21581937

chore(linear_algebra/multilinear/basic): move finite-dimensionality to a new file (#14198)

eric-wieser committed 3 years ago

1f0f9813

feat(analysis/locally_convex/with_seminorms): pull back `with_seminorms` along a linear inducing (#13549)

ADedecker committed 3 years ago

ae6f59d7

feat(group_theory/perm/list): Add missing `form_perm` lemmas (#13218)

MantasBaksys committed 3 years ago

ba38b47f

chore(set_theory/ordinal/{basic, arithmetic}): Inline instances (#14076)

vihdzp committed 3 years ago

da201ad4

feat(topology/metric_space): define a pseudo metrizable space (#14053)

urkud committed 3 years ago

600d8eaa

feat(algebra/homology): short exact sequences (#14009)

kim-em committed 3 years ago

e2eea550

feat(data/zmod/quotient): The minimal period equals the cardinality of the orbit (#14183)

tb65536 committed 3 years ago

3d279118

feat(number_theory/arithmetic_function): map a multiplicative function across a product (#14180)

b-mehta committed 3 years ago

3c87882b

feat(data/complex): real part of sum (#14177)

b-mehta committed 3 years ago

beee9ecb

chore(algebra/monoid_algebra): clean up some bad decidable arguments (#14175)

eric-wieser committed 3 years ago

d3e3eb84

test({data/{finset,set},order/filter}/pointwise): Ensure priority of the `ℕ` and `ℤ` actions (#14166)

YaelDillies committed 3 years ago

7db6ca99

feat(topology/separation): generalize a lemma (#14154)

urkud committed 3 years ago

f33b0847

split(algebra/hom/ring): Split off `algebra.ring.basic` (#14144)

YaelDillies committed 3 years ago

65bf1349

feat(data/polynomial/laurent): laurent polynomials are a module over polynomials (#14121)

adomani committed 3 years ago

4ae5e7a0

refactor(algebra/geom_sum): remove definition (#14120)

kim-em committed 3 years ago

46c42cc9

Older