Commits leanprover-community/mathlib3

fix(number_theory/cyclotomic/primitive_roots): speedup (#15804)

ericrbg committed 3 years ago

346cc93c

feat(algebra/periodic): `const_add`, `add_const`, `const_sub`, `sub_const` (#15782)

jsm28 committed 3 years ago

954f3e16

feat(algebra/category/Group/epi_mono): (mono)epimorphisms and (in)surjections are the same in `(Add)(Comm)Group` (#15496)

jjaassoonn committed 3 years ago

b74907b6

feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879)

mcdoll committed 3 years ago

a88bc4f7

feat(category_theory/limits): the constant functor preserves (co)limits (#15938)

TwoFX committed 3 years ago

03f58c52

feat(algebra/big_operators/basic): Sums and product in `additive`/`multiplicative` (#15898)

YaelDillies committed 3 years ago

26e8026f

feat(topology/algebra/group): add lemmas about `units` (#15921)

urkud committed 3 years ago

0bd4faee

feat(geometry/manifold/complex): holomorphic function on compact connected manifold is constant (#15667)

hrmacbeth committed 3 years ago

ec818836

doc(algebra/homology/homological_complex): fix doc and names (#15940)

riccardobrasca committed 3 years ago

e0b90625

chore(data/sign): simplify definition of multiplication (#15920)

vihdzp committed 3 years ago

fb478f66

chore(field_theory/polynomial_galois_group): golf `gal_action_hom` (#15919)

eric-wieser committed 3 years ago

6fcb704b

chore(tactic/doc_commands): simpler tactic_doc / library_note encoding (#15913)

digama0 committed 3 years ago

5be8529e

chore(data/real/ennreal): deduplicate `ennreal.nat_ne_top` (#15853)

j-loreaux committed 3 years ago

b9762673

chore(data/polynomial/degree/lemmas): rename lemmas that should have been renamed in an earlier PR (#15819)

adomani committed 3 years ago

b353d8e9

feat(src/data/polynomial/degree/definitions.lean): a lemma about monic polynomials (#15818)

adomani committed 3 years ago

c9dc8c1f

feat(category/idempotents): extension of functors to the idempotent completion (#15746)

joelriou committed 3 years ago

e75326d4

feat(field_theory/splitting_field): Add `image_root_set` (#15743)

tb65536 committed 3 years ago

0a34b827

feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv (#15523)

fpvandoorn committed 3 years ago

4ece2ee4

feat(order/bounded_order): More `disjoint` lemmas (#15304)

YaelDillies committed 3 years ago

0271f812

feat(data/set/pointwise): add `mem_pow` and `mem_prod_list_of_fn` (#15049)

eric-wieser committed 3 years ago

77b8e3cc

chore(data/mv_polynomial/basic): generalize lemmas about evaluation at zero (#15929)

eric-wieser committed 3 years ago

c7963f40

feat(category_theory): functors preserving exactness are left and right exact (#15900)

javra committed 3 years ago

1eb1aff5

feat(order/rel_iso): `well_founded (quotient.lift₂ r H) ↔ well_founded r` (#15890)

vihdzp committed 3 years ago

acf8294d

refactor(algebra/field/basic): generalize some lemmas to division monoids (#15845)

jsm28 committed 3 years ago

7edb6d5d

feat(ring_theory/polynomial/chebyshev): general cleanup (#15799)

vihdzp committed 3 years ago

ab2c6a7b

feat(ring_theory/adjoin_root): adjoin_root is noetherian (#15737)

alexjbest committed 3 years ago

56734db1

chore(data/mv_polynomial/basic): missing injectivity lemmas (#15928)

eric-wieser committed 3 years ago

49cc82c8

feat(big_operators/basic): sum of count over finset.filter equals countp (#15393)

dtumad committed 3 years ago

11bd2a08

perf(number_theory/padics/hensel): squeeze simps (#15926)

vihdzp committed 3 years ago

a81ef2fd

chore(order/basic): move `Prop.partial_order` to `order/basic` (#15884)

vihdzp committed 3 years ago

7fbadc69