leanprover-community/mathlib

Pull Requests Commits

feat(group_theory/complement): Add more API for the action on left transversals (#13363)

tb65536 committed 4 years ago

15b764d8

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13362)

tb65536 committed 4 years ago

769ec8c8

chore(order/complete_lattice): General cleanup (#13323)

vihdzp committed 4 years ago

3676f11d

feat(category_theory): turn a split mono with cokernel into a biproduct (#13184)

javra committed 4 years ago

7bb10813

feat(number_theory/legendre_symbol): add directory legendre_symbol and move quadratic_reciprocity.lean into it (#13441)

MichaelStollBayreuth committed 4 years ago

2693ab58

feat(topology/unit_interval): add lemmas (#13344)

fpvandoorn committed 4 years ago

eb2780b6

chore(data/nat/factorial): tidy (#13436)

ericrbg committed 4 years ago

87f8076f

feat(data/mv_polynomial): add support_X_pow (#13435)

alexjbest committed 4 years ago

dac4f18f

feat(complex/roots_of_unity): extensionality (#13431)

ericrbg committed 4 years ago

1378eabf

chore(*): suggestions from the generalisation linter (#13092)

kim-em committed 4 years ago

2249a240

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

leanprover-community-bot committed 4 years ago

a5654710

feat(complex/arg): arg_eq_zero_iff (#13432)

ericrbg committed 4 years ago

b62626e5

chore(order/category/Preorder): reduce imports (#13301)

kim-em committed 4 years ago

0765994d

feat(data/polynomial/*): suggestions from the generalization linter (#13342)

kim-em committed 4 years ago

6f401acf

chore(algebra/polynomial/big_operators): drop some nontrivial assumptions (#13428)

Ruben-VandeVelde committed 4 years ago

76c969b7

feat(model_theory/encoding): Bundled encoding of terms (#13226)

awainverse committed 4 years ago

da13598d

feat(ring_theory/tensor_product): add assoc for tensor product as an algebra homomorphism (#13309)

alexjbest committed 4 years ago

99138604

feat(analysis/normed_space/basic): normed division algebras over ℝ are also normed algebras over ℚ (#13384)

eric-wieser committed 4 years ago

0c3f75bb

feat(model_theory/skolem, satisfiability): A weak Downward Loewenheim Skolem (#13141)

awainverse committed 4 years ago

50ff59ad

feat(model_theory/fraisse): Defines ultrahomogeneous structures, fixes Fraïssé limit definition (#12994)

awainverse committed 4 years ago

647aa5be

feat(order/bounded_order): Basic API for `subtype.order_bot` and `subtype.order_top` (#12904)

Paul-Lez committed 4 years ago

6f59d777

feat(category_theory/monoidal): define monoidal structure on the category of monoids in a braided monoidal category (#13122)

manzyuk committed 4 years ago

5b8bb9b4

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

leanprover-community-bot committed 4 years ago

1de6ce93

fix(combinatorics/simple_graph/connectivity): correctly generalized variables (#13405)

kmill committed 4 years ago

b0bd7716

refactor(set_theory/cofinality): Normalize names (#13400)

vihdzp committed 4 years ago

917fc964

chore(set_theory/*): Fix lint (#13399)

YaelDillies committed 4 years ago

ac7a356a

feat(order/conditionally_complete_lattice): Add `le_cSup_iff` (#13321)

vihdzp committed 4 years ago

8c9ee310

refactor(category_theory/shift): tighten scope of local attribute [reducible] (#13335)

kim-em committed 4 years ago

fb948808

feat(computability/{language/regular_expressions): Map along a function (#13197)

YaelDillies committed 4 years ago

f496ef4c

feat(topology/homotopy): Add definition of contractible spaces (#12731)

prakol16 committed 4 years ago

7ece83ed

Newer Older