leanprover-community/mathlib

Pull Requests Commits

feat(data/set/n_ary): Distributivity of `∩` (#17924)

YaelDillies committed 3 years ago

4a1bf948

chore(data/set/sigma): Fix lemma (#17929)

YaelDillies committed 3 years ago

41a38802

feat(number_theory/number_field/norm): add file (#17672)

riccardobrasca committed 3 years ago

ee0c179c

feat(measure_theory/measure/haar_lebesgue): Lebesgue measure coming from an alternating map (#17583)

sgouezel committed 3 years ago

f721cdca

chore(group_theory/perm/cycle/basic): Move declarations around (#17906)

YaelDillies committed 3 years ago

ec4bdab8

feat(algebra/group_power/order): add monotonicity lemmas (#17895)

eric-wieser committed 3 years ago

dd4c2044

chore(order/atoms): split out finiteness results (#17866)

Ruben-VandeVelde committed 3 years ago

c55911f6

feat(ring_theory/valuation/valuation_subring): Add `valuation_subring.comap` (#17310)

mkaratarakis committed 3 years ago

d8615108

feat(dynamics/fixed_points/basic): `x` is fixed by `fⁿ` if it is fixed by `f` (#17908)

YaelDillies committed 3 years ago

b0cd2099

feat(group_theory/subgroup/basic): add lemmas about `subgroup.map` (#17894)

urkud committed 3 years ago

2be0e5fd

fix(ci): do not fail when detecting ported files more than 40 commits old (#17914)

eric-wieser committed 3 years ago

a5c51665

refactor(data/set/intervals/monotone): split (#17893)

urkud committed 3 years ago

ac5a7cec

feat(logic/denumerable): Any two infinite countable types are equivalent (#17903)

YaelDillies committed 3 years ago

fc2ed6f8

feat(number_theory/modular_forms): Modular form definition (#13250)

AlexKontorovich committed 3 years ago

32d096dc

feat(linear_algebra/affine_space/independent): spans of two affine combinations (#17861)

jsm28 committed 3 years ago

ee00ca5e

feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901)

YaelDillies committed 3 years ago

bd59f822

refactor(linear_algebra/basic): use `bijective` in `linear_equiv.of_bijective` (#17897)

eric-wieser committed 3 years ago

6d584f17

fix(analysis/normed_space/basic): add back computable module instance (#17813)

eric-wieser committed 3 years ago

85158adc

feat(analysis/convex/cone/basic): submodules are convex cones (#17749)

eric-wieser committed 3 years ago

800f5229

feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767)

alreadydone committed 3 years ago

1c521b4f

feat(data/list/basic): add lemma map_eq_repeat_iff (#17832)

MichaelStollBayreuth committed 3 years ago

cf9386b5

feat(group_theory/perm/basic): `subtype_perm` is a monoid hom (#17816)

YaelDillies committed 3 years ago

4f4e7fa6

chore(data/list/range): split & reduce imports (#17887)

astrainfinita committed 3 years ago

9925a115

refactor(topology/algebra/ring): rename subring.subring_topological_closure to subring.le_topological_closure (#17649)

xroblot committed 3 years ago

43afc5ad

feat(algebra/module/big_operators): Product of sums (#17818)

YaelDillies committed 3 years ago

4e87c847

chore(data/multiset/nodup): remove dependency on `multiset.powerset` (#17888)

astrainfinita committed 3 years ago

036348ae

refactor(algebra/group/defs): use `is_left_cancel_mul` etc (#17884)

urkud committed 3 years ago

2e0975f6

chore(data/finset): remove unused imports (#17891)

astrainfinita committed 3 years ago

955890d3

chore(number_theory/ramification_inertia): make an argument explicit (#17890)

eric-wieser committed 3 years ago

68f41d3c

chore(number_theory/padics/padic_val): golf (#17885)

urkud committed 3 years ago

60fa54e7

Newer Older