leanprover-community/mathlib3

Pull Requests Commits

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

doc(data/countable/small): fix module docs (#15924)

urkud committed 3 years ago

dff563ec

feat(data/sign): more lemmas (#15917)

jsm28 committed 3 years ago

46ba96e7

feat(data/sym/sym2): `sym2.lift₂` (#15887)

vihdzp committed 3 years ago

a0c5aef8

feat(data/list/of_fn): last_of_fn (#15474)

pechersky committed 3 years ago

e992b757

feat(field_theory/polynomial_galois_group): add `mul_semiring_action` instance for `polynomial.gal` (#15914)

astrainfinita committed 3 years ago

9a4dde32

chore(data/multiset/basic): move theorems around (#15882)

vihdzp committed 3 years ago

1e594c77

feat(order/initial_seg): exchange `down` and `down'` (#15802)

vihdzp committed 3 years ago

0e9c7c16

chore(ring_theory/dedekind_domain): better, computable, defeq in `cancel_comm_monoid_with_zero` instance (#15752)

Vierkantor committed 3 years ago

530b948f

chore(order/well_founded): golf + rename variables (#15730)

vihdzp committed 3 years ago

05307825

Newer Older