Commits leanprover-community/mathlib3

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

chore(group_theory/free_abelian_group): remove is_add_monoid_hom (#13349)

kim-em committed 3 years ago

708e2dee

feat(algebra/group/basic|topology/connected): add two lemmas (#13345)

fpvandoorn committed 3 years ago

333e4be6

chore(set_theory/cardinal): Golf `mk_le_mk_mul_of_mk_preimage_le` (#13329)

vihdzp committed 3 years ago

56d63993

feat(model_theory/order): The theory of dense linear orders without endpoints (#13253)

awainverse committed 3 years ago

670735fc

feat(topology/algebra/algebra): define the topological subalgebra generated by an element (#13093)

dupuisf committed 3 years ago

34853a95