leanprover-community/mathlib

Pull Requests Commits

hrmacbeth committed 3 years ago

4ceff160

hrmacbeth committed 3 years ago

d0903e7b

doc(number_theory/padics/*): typo in references (#12229)

kbuzzard committed 3 years ago

7cc4eb9d

chore(analysis): rename times_cont_diff (#12227)

PatrickMassot committed 3 years ago

42388681

refactor(combinatorics/simple_graph/{basic,degree_sum}): move darts from degree_sum to basic (#12195)

kmill committed 3 years ago

541a1a02

feat(ring_theory/localization): add a fintype instance (#12150)

ericrbg committed 3 years ago

f6ec999f

feat(algebra/module,linear_algebra): some `restrict_scalars` lemmas (#12181)

Vierkantor committed 3 years ago

e89222a6

feat(algebra/group/{hom,prod}): has_mul and mul_hom.prod (#12110)

pechersky committed 3 years ago

2ab3e2fa

feat(topology/algebra/group): add subgroup lemmas (#12026)

mariainesdff committed 3 years ago

18d1bdfc

feat(topology/algebra/group): add continuity lemmas (#11975)

mariainesdff committed 3 years ago

b60b7904

feat(set_theory/ordinal): `Inf_empty` (#12226)

vihdzp committed 3 years ago

64c8d217

docs(set_theory/ordinal): Remove mention of `omin` from docs (#12224)

vihdzp committed 3 years ago

d990681c

feat(set_theory/ordinal_arithmetic): `out_nonempty_iff_ne_zero` (#12223)

vihdzp committed 3 years ago

f7b6f421

chore(analysis/specific_limits): simplify proof of `cauchy_series_of_le_geometric` (#12215)

ecstatic-morse committed 3 years ago

e50ebde5

chore(linear_algebra/basic): golf `linear_equiv.smul_of_unit` (#12190)

eric-wieser committed 3 years ago

48ddfd55

refactor(model_theory/terms_and_formulas): Improvements to basics of first-order formulas (#12091)

awainverse committed 3 years ago

6bb8f229

feat(/analysis/inner_product_space/pi_L2): `inner_matrix_row_row` (#12177)

hparshall committed 3 years ago

d054fcae

feat(analysis/inner_product_space/adjoint): is_self_adjoint_iff_inner… (#12113)

hparshall committed 3 years ago

d0c37a11

chore(*): rename `erase_dup` to `dedup` (#12057)

ericrbg committed 3 years ago

8f160018

refactor(topology/compacts): Turn into structures, use `set_like`, cleanup (#12035)

YaelDillies committed 3 years ago

35ef7700

chore(ring_theory/graded_algebra/basic): remove commutativity requirement (#12208)

eric-wieser committed 3 years ago

71da192c

chore(ring_theory): split `localization.lean` and `dedekind_domain.lean` (#12206)

Vierkantor committed 3 years ago

f0401b91

feat(mv_polynomial/basic): monomial_eq_monomial_iff (#12198)

ericrbg committed 3 years ago

deb5046b

feat(measure_theory/group/arithmetic): add `has_measurable_smul.op` and `has_measurable_smul₂.op` (#12196)

eric-wieser committed 3 years ago

8b09b0ec

feat(ring_theory/ideal/operations): remove unneeded assumptions from `smul_induction_on` (#12193)

eric-wieser committed 3 years ago

79c5de9a

feat(order/hom/basic): `order_iso_class` (#12157)

YaelDillies committed 3 years ago

f6d397fc

feat(topology/bases): disjoint unions of second-countable spaces are second-countable (#12061)

sgouezel committed 3 years ago

4c6b0de0

feat(topology/support): define topological support and compactly supported functions (#11923)

fpvandoorn committed 3 years ago

8413f078

feat(order/hom/lattice): Finitary join-/meet-preserving maps (#12149)

YaelDillies committed 3 years ago

80591d65

refactor(topology/*): Hom classes for continuous maps/homs (#11909)

YaelDillies committed 3 years ago

68efb10c

Older