leanprover-community/mathlib3

Pull Requests Commits

ADedecker committed 3 years ago

1af0a0b2

Eric's suggestions

ADedecker committed 3 years ago

c37ad93e

Quotient module is isomorphic to quotient group

ADedecker committed 3 years ago

e5802f91

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

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

Older