Commits leanprover-community/mathlib

feat(probability/stopping): if a filtration is sigma finite, then the measure restricted to the sigma algebra generated by a stopping time is sigma finite (#14752)

RemyDegenne committed 3 years ago

3091b91e

feat(measure_theory/measure/finite_measure_weak_convergence): Characterize weak convergence of finite measures in terms of integrals of bounded continuous real-valued functions. (#14578)

kkytola committed 3 years ago

72fbe5c3

chore(data/sigma/basic): make `sigma.reflect` universe-polymorphic (#14934)

eric-wieser committed 3 years ago

cf0649c5

chore(algebra/direct_sum/ring): add new `int_cast` and `nat_cast` fields to match `ring` and `semiring` (#14976)

eric-wieser committed 3 years ago

671c7c05

fix(linear_algebra/{exterior,clifford}_algebra/basic): add some missing namespaces (#14975)

eric-wieser committed 3 years ago

af8ca85d

feat(algebra/group/units): add decidability instance for `is_unit` (#14873)

MichaelStollBayreuth committed 3 years ago

d4f8a454

feat(set_theory/game/pgame): make `lt_iff_le_and_lf` true by def-eq (#14983)

vihdzp committed 3 years ago

0b18823c

refactor(order/upper_lower): Reverse the order on `upper_set` (#14982)

YaelDillies committed 3 years ago

894f92bc

feat(combinatorics/simple_graph/clique): The set of cliques (#14827)

YaelDillies committed 3 years ago

f63d925e

refactor(set_theory/cardinal/*): `cardinal.sup` → `supr` (#14569)

vihdzp committed 3 years ago

f2b108e8

feat(data/nat/totient): more general multiplicativity lemmas for totient (#14842)

stuart-presnell committed 3 years ago

33112c45

feat(analysis/convex/stone_separation): Stone's separation theorem (#14677)

YaelDillies committed 3 years ago

381733a5

docs(linear_algebra/invariant_basis_number): Drop a TODO (#14973)

urkud committed 3 years ago

4111ed94

feat(analysis/special_functions/trigonometric/angle): topology (#14969)

jsm28 committed 3 years ago

ca070dd6

feat(set_theory/surreal/basic): add `numeric.mk` lemma, golf (#14962)

vihdzp committed 3 years ago

28a6f0ac

feat(combinatorics/catalan): definition and equality of recursive and explicit definition (#14869)

Julian-Kuelshammer committed 3 years ago

54352be4

feat({data/{finset,set},order/filter}/pointwise): Missing `smul_comm_class` instances (#14963)

YaelDillies committed 3 years ago

ee7a8863

feat: `add_monoid_with_one`, `add_group_with_one` (#12182)

gebner committed 3 years ago

32b08ef8

feat(data/zmod/algebra): add subsingleton instance for zmod-algebras (#14946)

ericrbg committed 3 years ago

871fcd87

feat(set_theory/ordinal/notation): fast growing hierarchy (#14072)

digama0 committed 3 years ago

e0ecaa9e

feat(data/{finset,set}/basic): More `∪`/`∩` laws (#14952)

YaelDillies committed 3 years ago

cfbb97f7

feat(data/set/lattice): Preimages are disjoint iff the sets are disjoint (#14951)

YaelDillies committed 3 years ago

ccb1cf38

feat(order/symm_diff): The symmetric difference is involutive (#14959)

YaelDillies committed 3 years ago

72cff840

refactor(*): Use `finset.Iix`/`finset.Ixi` (#14448)

YaelDillies committed 3 years ago

b8c3e61b

feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816)

YaelDillies committed 3 years ago

7ee73e4a

feat(algebra/field/basic): Semifields (#14683)

YaelDillies committed 3 years ago

88127521

feat(analysis/normed*): add instances about balls and spheres (#14808)

urkud committed 3 years ago

f9571f0f

chore(*): golf (#14939)

urkud committed 3 years ago

6f923bd9

feat(linear_algebra/clifford_algebra/of_alternating): extend alternating maps to the exterior algebra (#14803)

eric-wieser committed 3 years ago

07c83c81

feat(representation_theory/character): characters of representations (#14453)

antoinelab01 committed 3 years ago

4fd263ba