Commits leanprover-community/mathlib

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

feat(algebra/algebraic_card): Cardinality of algebraic numbers (#12869)

vihdzp committed 3 years ago

ed919b61

feat(algebraic_geometry/projective_spectrum): Proj as a locally ringed space (#12773)

jjaassoonn committed 3 years ago

6bc2bd6e

feat(ring_theory/valuation/valuation_ring): Valuation rings and their associated valuation. (#12719)

adamtopaz committed 3 years ago

72e1a9ee

feat(data/complex/basic): add a few lemmas (#13354)

urkud committed 3 years ago

b889567e

chore(*): more assumptions to lemmas that are removable (#13364)

alexjbest committed 3 years ago

0783742a

chore(algebra/big_operators/intervals): Move and golf sum_range_sub_sum_range (#13359)

BoltonBailey committed 3 years ago

56f6c8e8

feat(topology/metric_space/basic): some lemmas about dist (#13343)

fpvandoorn committed 3 years ago

603db27a

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `mul_one_class` `preorder` (#13299)

astrainfinita committed 3 years ago

cbea7e1f

feat(group_theory/complement): Criterion for complementary subgroups (#13292)

tb65536 committed 3 years ago

e3db2e78

fix(category_theory/elements): speed up `groupoid_of_elements` (#13372)

alreadydone committed 3 years ago

fdd68d9b

chore(algebra/module/basic): generalize to add_monoid_hom_class (#13346)

eric-wieser committed 3 years ago

bf1b813e

feat(data/list/basic): add a theorem about last and append (#13336)

sorawee committed 3 years ago

955cb8e6

feat(algebra/order/monoid_lemmas_zero_lt): add lemmas assuming `mul_zero_class` `preorder` (#13297)

astrainfinita committed 3 years ago

10a3faa4

feat(data/polynomial/algebra_map): remove some lemmas about `aeval`, add `protected` on `polynomial.map_list_prod` (#13294)

astrainfinita committed 3 years ago

fe1c78af

feat(analysis/convex/strict_convex_space): Ray characterization of `∥x - y∥` (#13293)

YaelDillies committed 3 years ago

483b7df9

feat(topology/uniform_space/uniform_convergence_topology): define the uniform structure of uniform convergence (#13073)

ADedecker committed 3 years ago

f1c98ba8