Commits leanprover-community/mathlib

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

Ruben-VandeVelde committed 3 years ago

76c969b7

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

awainverse committed 3 years ago

da13598d

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

alexjbest committed 3 years ago

99138604

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

eric-wieser committed 3 years ago

0c3f75bb

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

awainverse committed 3 years ago

50ff59ad

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

awainverse committed 3 years ago

647aa5be

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

Paul-Lez committed 3 years ago

6f59d777

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

manzyuk committed 3 years ago

5b8bb9b4

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

leanprover-community-bot committed 3 years ago

1de6ce93

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

kmill committed 3 years ago

b0bd7716

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

vihdzp committed 3 years ago

917fc964

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

YaelDillies committed 3 years ago

ac7a356a

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

vihdzp committed 3 years ago

8c9ee310

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

kim-em committed 3 years ago

fb948808

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

YaelDillies committed 3 years ago

f496ef4c

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

prakol16 committed 3 years ago

7ece83ed

feat(category_theory/monoidal): prove that in a braided monoidal category unitors and associators are monoidal natural transformations (#13121)

manzyuk committed 3 years ago

94a52c43

feat(order/filter/cofinite): add lemmas, golf (#13394)

urkud committed 3 years ago

78ea75a0

feat(ring_theory/valuation/valuation_subring): Valuation subrings of a field (#12741)

adamtopaz committed 3 years ago

da4ec7e1

feat(number_theory/qudratic_reciprocity): change type of `a` in API lemmas to `int` (#13393)

MichaelStollBayreuth committed 3 years ago

e72f275d

chore(*): remove instance arguments that are inferrable from earlier (#13386)

alexjbest committed 3 years ago

3bbb847e

feat(analysis/normed_space/exponential): exponentials of negations, scalar actions, and sums (#13036)

eric-wieser committed 3 years ago

116ac710

feat(ring_theory/algebraic): Rational numbers are algebraic (#13367)

vihdzp committed 3 years ago

949021d6

feat(category_theory/monoidal): define a monoidal structure on the tensor product functor of a braided monoidal category (#13150)

manzyuk committed 3 years ago

c994ab3f

doc(model_theory/order): typo in docstrings (#13390)

fpvandoorn committed 3 years ago

4c0a2744

fix(measure_theory/function/lp_space): fix an instance diamond in `measure_theory.Lp.has_edist` (#13388)

eric-wieser committed 3 years ago

0c8b8084

feat(algebra/direct_sum): Reindexing direct sums (#13076)

pbazin committed 3 years ago

c21561a0

chore(*/parity): Generalize lemmas and clarify names (#13268)

YaelDillies committed 3 years ago

745099b8

feat(counterexamples/pseudoelement): add counterexample to uniqueness in category_theory.abelian.pseudoelement.pseudo_pullback (#13387)

riccardobrasca committed 3 years ago

4b45a714

chore(category_theory/closed/monoidal): correct error in doc string (#13385)

kim-em committed 3 years ago

73ec5b27