leanprover-community/mathlib

Pull Requests Commits

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

refactor(field_theory,ring_theory): generalize adjoin_root.equiv to `power_basis` (#8726)

Vierkantor committed 4 years ago

6bd6c11b

feat(ring_theory/dedekind_domain): prime elements of `ideal A` are the prime ideals (#8718)

Vierkantor committed 4 years ago

3de385a2

feat(data/matrix/kronecker): add two lemmas (#8700)

faenuccio committed 4 years ago

f1b6c8fd

refactor(topology/algebra/ring): `topological_ring` extends `topological_add_group` (#8709)

urkud committed 4 years ago

5335c671

feat(algebra/pointwise): instances in locale pointwise (#8689)

fpvandoorn committed 4 years ago

11516119

feat(data/list/perm): nodup_permutations (#8616)

pechersky committed 4 years ago

efa34dc6

feat(linear_algebra/clifford_algebra/equivs): there is a clifford algebra isomorphic to every quaternion algebra (#8670)

eric-wieser committed 4 years ago

41f7b5ba

chore(data/set/function): remove useless @[simp] (#8736)

kim-em committed 4 years ago

40b7dc75

feat(algebra/ordered_monoid): generalize {min,max}_mul_mul_{left,right} (#8725)

pechersky committed 4 years ago

cb3d5db3

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

leanprover-community-bot committed 4 years ago

e23e6ebd

feat(measure_theory/decomposition/lebesgue): the Lebesgue decomposition theorem (#8687)

kex-y committed 4 years ago

ce965a55

feat(algebra): generalize `ring_hom.map_dvd` (#8722)

Vierkantor committed 4 years ago

67501f68

chore(lie/semisimple): tweak `lie_algebra.subsingleton_of_semisimple_lie_abelian` (#8728)

ocfnash committed 4 years ago

e6e5718a

docs(overview): nilpotent and presented groups (#8711)

PatrickMassot committed 4 years ago

31d55491

fix(tactic/tfae): remove unused arg in tfae_have (#8727)

digama0 committed 4 years ago

5b5b432e

chore(algebra/module/basic): golf a proof (#8723)

eric-wieser committed 4 years ago

e0656d12

feat(ring_theory/power_basis): `pb.minpoly_gen = minpoly pb.gen` (#8719)

Vierkantor committed 4 years ago

579ec7d3

feat(tactic/lint): add universe linter (#8685)

fpvandoorn committed 4 years ago

fefdcf52

docs(order/filter/partial): add module docstring (#8620)

YaelDillies committed 4 years ago

3453f7a8

chore(algebra/associated): use more dot notation (#8556)

Vierkantor committed 4 years ago

90fc0641

chore(*): flip various `subsingleton_iff`, `nontrivial_iff` lemmas and add `simp` (#8703)

ocfnash committed 4 years ago

508b13ee

refactor(algebra/algebra/basic): move restrict_scalars into more appropriate files (#8712)

eric-wieser committed 4 years ago

450c2d08

feat(measure_theory/measure/measure_space): add formula for `(map f μ).to_outer_measure` (#8714)

urkud committed 4 years ago

0c145d82

chore(topology/maps): add tendsto_nhds_iff lemmas (#8693)

YaelDillies committed 4 years ago

4df3fb9e

Newer Older