leanprover-community/mathlib3

Pull Requests Commits

feat(*): bump to lean 3.50.0

gebner committed 3 years ago

d829441c

feat(algebra/star/basic): add ring_hom.has_involutive_star (#17904)

xroblot committed 3 years ago

daf8adf1

feat(combinatorics/double_counting): Special cases (#17647)

YaelDillies committed 3 years ago

aba57d4d

feat(order/succ_pred/basic): `a ⩿ b → b ≤ succ a` (#17940)

YaelDillies committed 3 years ago

f2c46488

feat(ring_theory/power_series): `X s` commutes with any power series (#17935)

urkud committed 3 years ago

7d6cd041

feat(dynamics/ergodic/add_circle): generalise `add_circle.ae_empty_or_univ_of_forall_vadd_eq_self` slightly (#17907)

ocfnash committed 3 years ago

ae3588fa

feat(measure_theory/covering/liminf_limsup): add lemma `blimsup_cthickening_mul_ae_eq` (#17803)

ocfnash committed 3 years ago

1897d7de

fix(tactic/assert_exists): use more unique names (#17916)

eric-wieser committed 3 years ago

90367774

feat(ring_theory/dedekind_domain/factorization): add factorization lemmas (#17915)

mariainesdff committed 3 years ago

ae0d10f6

feat(data/set/pointwise/smul): `a • (s \ t) = a • s \ a • t` (#17927)

YaelDillies committed 3 years ago

ae193735

chore(algebra/big_operators/part_enat): drop file (#17934)

urkud committed 3 years ago

a2efed67

feat(data/prod/basic): `prod.lex` is trichotomous (#17931)

YaelDillies committed 3 years ago

198161d8

feat(data/fin/basic): lemmas commuting `cast_add` and `nat_add` (#17917)

eric-wieser committed 3 years ago

d97d4fac

refactor(data/set/intervals): Generalize `set.interval` to lattices (#17776)

YaelDillies committed 3 years ago

b8858394

Revert "feat(ring_theory/power_series): `X s` commutes with any power series"

urkud committed 3 years ago

27982536

feat(ring_theory/power_series): `X s` commutes with any power series

urkud committed 3 years ago

f1adf6ad

chore(group_theory/group_action/prod): Fix typo in `to_additive` attribute. (#17930)

adamtopaz committed 3 years ago

46ae64dc

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

Older