leanprover-community/mathlib3

Pull Requests Commits

thorimur committed 2 years ago

89466165

thorimur committed 2 years ago

4468bcbb

chore: remove uses of and.rec (#18123)

ChrisHughes24 committed 2 years ago

6133ae2d

feat(analysis/bounded_variation): some lemmas (#18108)

bottine committed 2 years ago

a2d2e189

feat(data/mv_polynomial/*): Simple `•` lemmas (#18084)

YaelDillies committed 2 years ago

65902a4a

chore(data/real/ennreal): Protect ambiguous lemmas (#18076)

YaelDillies committed 2 years ago

11c2b8c1

feat(group_theory/perm/cycle/basic): Cycle on a set (#17899)

YaelDillies committed 2 years ago

b8683232

chore(algebra/order/archimedean): add `sub` variations of `add` lemmas (#18103)

eric-wieser committed 2 years ago

6f413f3f

refactor(algebra/order/to_interval_mod): state more results in terms of interval sets (#18102)

eric-wieser committed 2 years ago

e017e666

chore(group_theory/presented_group): generalize universe (#18115)

alreadydone committed 2 years ago

7b78d177

feat(ring_theory/class_group): add class_group.mk_eq_mk (#18034)

Multramate committed 2 years ago

09d74faa

feat(linear_algebra/span): add submodule.mem_span lemmas (#18100)

Multramate committed 2 years ago

2f7b36ab

refactor(ring_theory/fractional_ideal): refactor coe_to_fractional_ideal lemmas (#18055)

Multramate committed 2 years ago

2f588be3

feat(order/hom/complete_lattice): inf as an Inf_hom and sup as a Sup_hom (#18023)

mans0954 committed 2 years ago

c8a43b45

feat(algebra/order/absolute_value): Absolute values are multiplicative ring norms (#16919)

YaelDillies committed 2 years ago

7ea60478

feat(order/partial_sups): add csupr lemmas (#18053)

eric-wieser committed 2 years ago

dd71334d

feat(algebraic_geometry/elliptic_curve/weierstrass): define ideals of the coordinate ring associated to the X and Y coordinates (#18038)

Multramate committed 2 years ago

0b9c21e2

chore(data/int/order/basic): Fix lemma name (#17967)

YaelDillies committed 2 years ago

e1bccd6e

fix(algebra/group_power/lemmas): fix the name of sub_one_zsmul (#18109)

eric-wieser committed 2 years ago

02c4026c

feat(ring_theory/ideal/*): add more ideal.span lemmas (#18079)

Multramate committed 2 years ago

51a845f0

feat(ring_theory/ideal/operations): add span_singleton_mul_left lemmas (#18056)

Multramate committed 2 years ago

ba2d8fb3

feat(order/complete_lattice): missing API lemmas about the prod instance (#18029)

eric-wieser committed 2 years ago

5709b0d8

chore(algebra/module/linear_map): move `map_sum` lemmas (#18106)

hrmacbeth committed 2 years ago

40acfb6a

feat(analysis/fourier): convergence of Fourier series (#17913)

loefflerd committed 2 years ago

247a102b

feat(measure_theory/integral): "integral_prod_mul" for complex coefficients (#18085)

loefflerd committed 2 years ago

7c60702a

feat(data/{set,finset}/basic): Convenience lemmas (#17957)

YaelDillies committed 2 years ago

bc7d81be

feat(field_theory/chevalley_warning): Binary version (#18083)

YaelDillies committed 2 years ago

e001509c

chore(algebra/group_ring_action/invariant): streamline imports (#18092)

hrmacbeth committed 2 years ago

e7bab9a8

chore(number_theory/pell): golf, use tactic mode (#18091)

urkud committed 2 years ago

5a1fa97e

feat(topology/instances/add_circle): generalize `homeo_Icc_quot` from ℝ to archimedean groups (#17983)

alreadydone committed 2 years ago

940d3713

Older