leanprover-community/mathlib

Pull Requests Commits

b-mehta committed 3 years ago

159d6144

pi is irrational

b-mehta committed 3 years ago

eb9f650a

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

chore(algebra/order/monoid): golf an instance (#14184)

urkud committed 3 years ago

2370d104

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

leanprover-community-bot committed 3 years ago

f1c08cde

refactor(algebra/{group_power/{basic,lemmas},group_with_zero/power}): Generalize lemmas to division monoids (#14102)

YaelDillies committed 3 years ago

737784ef

feat(number_theory/legendre_symbol/*): move characters on `zmod n` to new file, add API, improve a proof (#14178)

MichaelStollBayreuth committed 3 years ago

89f2760f

chore(geometry/manifold/algebra/left_invariant_derivation): golf some proofs (#14172)

eric-wieser committed 3 years ago

93dca41a

refactor(data/pi/lex): Use `lex`, provide notation (#14164)

YaelDillies committed 3 years ago

4586a97a

feat(data/bool/basic): Kaminski's equation (#14159)

slerpyyy committed 3 years ago

009669cb

split(data/set/semiring): Split off `data.set.pointwise` (#14145)

YaelDillies committed 3 years ago

909b6732

feat(order/filter/at_top_bot): use weaker TC assumptions, add lemmas (#14105)

urkud committed 3 years ago

a9e74ab7

refactor(algebra/hom/group): Generalize `map_inv` to division monoids (#14134)

YaelDillies committed 3 years ago

844a4f7b

fix(tactic/core): Make the `classical` tactic behave like `open_locale classical` (#14122)

eric-wieser committed 3 years ago

90659cbe

chore(set_theory/game/pgame): minor golf (#14171)

vihdzp committed 3 years ago

df64e5e5

chore(group_theory/specific_groups/cyclic): golf `card_order_of_eq_totient_aux₁` and `card_order_of_eq_totient_aux₂` (#14161)

stuart-presnell committed 3 years ago

f4c67ee5

feat(data/int/basic): add theorem `int.div_mod_unique` (#14158)

Faris999 committed 3 years ago

a5975e73

chore(ring_theory/ideal/local_ring): golf some proofs, add missing lemma (#14157)

Ruben-VandeVelde committed 3 years ago

f7a7c272

feat(data/zmod/quotient): `orbit (zpowers a) b` is a cycle of order `minimal_period ((•) a) b` (#14124)

tb65536 committed 3 years ago

55b31e05

Older