leanprover-community/mathlib

Pull Requests Commits

remove non-unital stuff for now

dupuisf committed 3 years ago

645a192b

functional calculus draft

dupuisf committed 3 years ago

b60b72cb

dupuisf committed 3 years ago

47e5a71f

readd the defs...

dupuisf committed 3 years ago

8acbd511

add weak dual namespace fixes + extra lemmas

dupuisf committed 3 years ago

1cb8e142

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

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

Older