Commits leanprover-community/mathlib3

feat(algebra/homology): some elementwise lemmas (#12997)

kim-em committed 3 years ago

eba31b58

feat(algebra/*): coe_to_equiv_symm simp lemmas (#12996)

kim-em committed 3 years ago

dacf0490

feat(measure_theory/functions/strongly_measurable): almost everywhere strongly measurable functions (#12985)

sgouezel committed 3 years ago

f0c15be6

chore(data/polynomial/ring_division): remove nontrivial assumptions (#12984)

eric-wieser committed 3 years ago

fd2c6c47

feat({ring_theory,group_theory}/localization): add some small lemmas for localisation API (#12861)

jjaassoonn committed 3 years ago

c0421e76

feat(ring_theory/localization): lemmas about `Frac(R)`-spans (#12425)

Vierkantor committed 3 years ago

1ebb2060

doc(data/polynomial/field_division): fix broken docstring links (#12981)

eric-wieser committed 3 years ago

e48f2e82

doc({linear_algebra,matrix}/charpoly): add crosslinks (#12980)

eric-wieser committed 3 years ago

d31410ab

feat(topology/continuous_on): add `set.maps_to.closure_of_continuous_on` (#12975)

urkud committed 3 years ago

597cbf10

feat(data/list/big_operators): add multiplicative versions (#12966)

urkud committed 3 years ago

ff72aa22

feat(data/polynomial/ring_division): `mem_root_set_iff` (#12963)

vihdzp committed 3 years ago

443c239d

chore(data/matrix/basic): square matrices over a non-unital ring form a non-unital ring (#12913)

eric-wieser committed 3 years ago

162d83fc

feat(set_theory/cardinal): `cardinal.to_nat` is order-preserving on finite cardinals (#12763)

tb65536 committed 3 years ago

c030dd2a

feat(set_theory/cofinality): Lemmas relating `cof` to `lsub` and `blsub` (#12316)

vihdzp committed 3 years ago

2873b7ac

feat(topology/continuous/algebra) : giving `C(α, M)` a `has_continuous_mul` and a `has_continuous_smul` structure (#11261)

laughinggas committed 3 years ago

b7d6b3aa

feat(order/hom/*): equivalences mapping morphisms to their dual (#12888)

YaelDillies committed 3 years ago

77110125

chore(test/matrix): clean up an unused argument (#12986)

alexjbest committed 3 years ago

587af996

feat(measure_theory/measure): add some simp lemmas, golf (#12974)

urkud committed 3 years ago

562bbf52

feat(data/list/pairwise): `pairwise_of_forall_mem_list` (#12968)

vihdzp committed 3 years ago

4b05a42d

chore(analysis/analytic/basic): golf (#12965)

urkud committed 3 years ago

73a9c27f

feat(analysis/normed_space): generalize some lemmas (#12959)

urkud committed 3 years ago

33afea82

feat(data/polynomial/erase_lead + data/polynomial/reverse): rename an old lemma, add a stronger one (#12909)

adomani committed 3 years ago

c65d8079

feat(analysis/inner_product_space): an inner product space is strictly convex (#12790)

urkud committed 3 years ago

7a1e0f20

chore(data/polynomial/degree/lemmas + data/polynomial/ring_division): move lemmas, reduce assumptions, golf (#12858)

adomani committed 3 years ago

1e72d86f

feat(analysis/von_neumann): concrete and abstract definitions of a von Neumann algebra (#12329)

kim-em committed 3 years ago

e5cd2ea1

feat(data/zmod/basic): add `int_coe_eq_int_coe_iff_dvd_sub` (#12944)

MichaelStollBayreuth committed 3 years ago

1494a9b2

feat(measure_theory/measure/measure_space): remove measurable_set assumption in ae_measurable.subtype_mk (#12978)

sgouezel committed 3 years ago

d620ad3c

chore(model_theory/*): Split up big model theory files (#12918)

awainverse committed 3 years ago

2c6df07f

chore(scripts): update nolints.txt (#12971)

leanprover-community-bot committed 3 years ago

57a5fd72

chore(data/set/intervals/ord_connected): Golf proof (#12923)

vihdzp committed 3 years ago

664247fc