Commits leanprover-community/mathlib3

wip(data/subtype_instances): introduce closed_under predicate typeclasses

eric-wieser committed 4 years ago

38a5388c

doc(data/semiquot): reformat module doc properly, and add missing doc strings (#7773)

kim-em committed 4 years ago

3870896a

docs(data/mllist): fix module doc, and add all doc strings (#7772)

kim-em committed 4 years ago

abe25e96

feat(measure_theory/tactic): add measurability tactic (#7756)

RemyDegenne committed 4 years ago

d9b91f3b

chore(geometry/euclidean/circumcenter): remove two `have`s in a proof (#7852)

adomani committed 4 years ago

8e25717f

chore(measure_theory/set_integral): put the definition of integrable_on into a new file (#7842)

RemyDegenne committed 4 years ago

d0ed2a42

feat(algebra/ordered_group): `-abs a ≤ a` (#7839)

benjamindavidson committed 4 years ago

764e878e

fix(*): make some non-instances reducible (#7835)

fpvandoorn committed 4 years ago

a9d4f3d4

chore(algebra/field_power, data/set/intervals/basic): simpler proofs in the first file, fewer parentheses in the second one (#7831)

adomani committed 4 years ago

20efef78

chore(measure_theory/outer_measure): add extend_eq_top (#7827)

eric-wieser committed 4 years ago

02d5370a

docs(order/bounded_lattice): add module docstring (#7799)

YaelDillies committed 4 years ago

fa7c6da2

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

leanprover-community-bot committed 4 years ago

55abf1a4

feat(ring_theory): every left-noetherian ring satisfies the strong rank condition (#7711)

kim-em committed 4 years ago

86766851

feat(measure_theory/interval_integral): integration by substitution / change of variables (#7273)

benjamindavidson committed 4 years ago

47ad6800

refactor(algebra/module/projective) make is_projective a class (#7830)

riccardobrasca committed 4 years ago

faa58e51

feat(topology/category/limits): Topological bases in cofiltered limits (#7820)

adamtopaz committed 4 years ago

c210d0fd

feat(data/finsupp): generalize finsupp.has_scalar to require only distrib_mul_action instead of semimodule (#7819)

eric-wieser committed 4 years ago

34c433d9

feat(ring_theory/localization): Make local_ring_hom more flexible (#7787)

justus-springer committed 4 years ago

393f6389

feat(topology/instances/ereal): more on ereal, notably its topology (#7765)

sgouezel committed 4 years ago

5c6d3bce

feat(measure_theory/integration): a measurable function is a series of simple functions (#7764)

sgouezel committed 4 years ago

75c81dee

feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs (#7754)

awainverse committed 4 years ago

39406bb9

chore(mv_polynomial/equiv): speed up elaboration by adjusting priorities (#7840)

sgouezel committed 4 years ago

42c42370

chore(data/fintype/basic): add fintype instance for `is_empty` (#7692)

ericrbg committed 4 years ago

320da57a

feat(category/limits): kernel.map (#7623)

kim-em committed 4 years ago

6e675366

feat(algebra/periodic): define periodicity (#7572)

benjamindavidson committed 4 years ago

fb72599b

feat(specific_groups/alternating_group): The alternating group on 5 elements is simple (#7502)

awainverse committed 4 years ago

e55d470c

feat(linear_algebra/quadratic_form): Complex version of Sylvester's law of inertia (#7416)

kex-y committed 4 years ago

fa7b5f20

feat(algebra/ring/basic): define non-unital, non-associative rings (#6786)

ocfnash committed 4 years ago

ef7aa94e

feat(order/symm_diff): symmetric difference operator (#6469)

bryangingechen committed 4 years ago

1eb3ae42

feat(data/fintype/basic): The cardinality of a set is at most the cardinality of the universe (#7823)

tb65536 committed 4 years ago

136e0d68