Commits leanprover-community/mathlib

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

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