leanprover-community/mathlib3

Pull Requests Commits

j-loreaux committed 2 years ago

Verified c84e5f97

implement forgetful inheritance

j-loreaux committed 2 years ago

Verified 920af275

remove extraneous bits

j-loreaux committed 2 years ago

Verified 976dba71

add unitization.star_lift

j-loreaux committed 2 years ago

Verified 09be2f24

generalize unitization.lift and other lemmas to semirings

j-loreaux committed 2 years ago

Verified a1cca04a

add a few things

j-loreaux committed 2 years ago

Verified d5421e94

first pass at the norm on the minimal unitization

j-loreaux committed 2 years ago

Verified 296a1b7b

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

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

Older