leanprover-community/mathlib

Pull Requests Commits

feat(measure_theory/strongly_measurable): define strongly measurable functions (#8623)

RemyDegenne committed 4 years ago

86fccaab

chore(algebra/big_operators): weaken assumption for multiset.exists_smul_of_dvd_count (#8758)

Ruben-VandeVelde committed 4 years ago

802859f2

feat(group_action/defs): add missing comp_hom smul instances (#8707)

eric-wieser committed 4 years ago

1efa3673

feat(ring_theory): the trace of an integral element is integral (#8702)

Vierkantor committed 4 years ago

4113db58

Revert "feat(field_theory/intermediate_field): generalize `algebra` instances"

Vierkantor committed 4 years ago

159e34ee

feat(field_theory/intermediate_field): generalize `algebra` instances

Vierkantor committed 4 years ago

4b525bf2

chore(tactic/rewrite_search): reuse rw_rules_p parser (#8752)

digama0 committed 4 years ago

902d3ac9

feat(analysis/calculus/deriv): prove `deriv_inv` at `x = 0` as well (#8748)

urkud committed 4 years ago

28a360a6

feat(topology/metric_space/basic): `emetric.ball x ∞ = univ` (#8745)

urkud committed 4 years ago

1c60e618

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

leanprover-community-bot committed 4 years ago

0e0a2404

chore(order/complete_lattice): golf some proofs (#8746)

urkud committed 4 years ago

ee3f8b8d

doc(tactic/simps): typo (#8751)

fpvandoorn committed 4 years ago

84554339

feat(algebra/algebra): `alg_{hom,equiv}.restrict_scalars` is injective (#8743)

Vierkantor committed 4 years ago

6fe5b552

doc({topology.algebra.weak_dual_topology, analysis.normed_space.weak_dual}): fix docstrings (#8710)

kkytola committed 4 years ago

e0bf9a16

feat(algebra/ordered_sub): define truncated subtraction in general (#8503)

fpvandoorn committed 4 years ago

23cf025c

feat(data/nat/pairing): add some `nat.pair` lemmas (#8740)

kex-y committed 4 years ago

0860c415

fix(transform_decl): fix namespace bug (#8733)

fpvandoorn committed 4 years ago

e6fda2ac

doc(tactic/simps): expand (#8729)

fpvandoorn committed 4 years ago

9a249eef

feat(topology/compact_open): the family of constant maps collectively form a continuous map (#8721)

ocfnash committed 4 years ago

6a83c7da

chore(topology/continuous_function/compact): relax typeclass assumptions for metric space structure on C(X, Y) (#8717)

ocfnash committed 4 years ago

3ac609b9

feat(topology/{continuous_function/bounded, metric_space/algebra}): new mixin classes (#8580)

hrmacbeth committed 4 years ago

0d59511a

feat(data/list/min_max): maximum is a fold, bounded prod (#8543)

pechersky committed 4 years ago

26590e97

feat(algebra/monoid_algebra): add_monoid_algebra.op_{add,ring}_equiv (#8536)

pechersky committed 4 years ago

4e7e7df8

feat(model_theory/basic): more substructure API, including subtype, map, and comap (#7937)

awainverse committed 4 years ago

15444e1f

chore(set/function): remove reducible on eq_on (#8738)

kim-em committed 4 years ago

a47d49db

doc(tactic/monotonicity): bad ac_mono syntax doc (#8734)

digama0 committed 4 years ago

02b90ab4

fix(algebra/algebra/restrict_scalars): Remove a bad instance (#8732)

eric-wieser committed 4 years ago

83c78217

feat(analysis/normed_space/affine_isometry): new file, bundled affine isometries (#8660)

hrmacbeth committed 4 years ago

c0f16d26

feat(ring_theory): define the ideal class group (#8626)

Vierkantor committed 4 years ago

d1b34f7b

chore({group,ring}_theory/sub{group,monoid,ring,semiring}): Add missing scalar action typeclasses (#8731)

eric-wieser committed 4 years ago

a0aee51a

Newer Older