leanprover-community/mathlib

Pull Requests Commits

urkud committed 3 years ago

1a8c9df0

urkud committed 3 years ago

62156816

urkud committed 3 years ago

284cc0ee

urkud committed 3 years ago

0c8d701e

urkud committed 3 years ago

9b3fb304

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

feat(number_theory/cyclotomic): alg-closed fields are cyclotomic extensions over themselves (#13366)

ericrbg committed 3 years ago

ef8e256d

chore(category_theory/preadditive/biproducts): Speed up `biprod.column_nonzero_of_iso` (#13383)

YaelDillies committed 3 years ago

5534e246

refactor(control/fold): don't use is_monoid_hom (#13350)

kim-em committed 3 years ago

4bcc5325

feat(order/filter/pointwise): Missing pointwise operations (#13170)

YaelDillies committed 3 years ago

8b27c457

fix(counterexamples): typo in module docstring (#13378)

jcommelin committed 3 years ago

99849606

feat(topology/bornology/basic): review (#13374)

urkud committed 3 years ago

36bafae8

feat(ring_theory/ideal): generalize `x mod I ∈ J mod I ↔ x ∈ J` (#13358)

Vierkantor committed 3 years ago

d065fd4a

feat(ring_theory/unique_factorization_domain): `factors x = normalized_factors x` (#13356)

Vierkantor committed 3 years ago

c8835190

feat(data/multiset): lemmas on intersecting a multiset with `repeat x n` (#13355)

Vierkantor committed 3 years ago

85588f87

refactor(ring_theory/free_comm_ring): don't use is_ring_hom (#13352)

kim-em committed 3 years ago

f7fe7dd0

feat(order/filter/at_top_bot): add more `disjoint` lemmas (#13351)

urkud committed 3 years ago

fd53ce0f

Older