leanprover-community/mathlib

Pull Requests Commits

algebra algebra

b-mehta committed 4 years ago

Verified 5126ba02

feat(linear_algebra/prod): add coprod_map_prod (#8220)

eric-wieser committed 4 years ago

a7b660e4

chore(measure_theory/measure_space): untangle `probability_measure`, `finite_measure`, and `has_no_atoms` (#8222)

eric-wieser committed 4 years ago

13486fe5

feat(data/finset/noncomm_prod): noncomm_prod_union_of_disjoint (#8169)

pechersky committed 4 years ago

b10062e7

feat(data/nat/basic): lt_one_iff (#8224)

pechersky committed 4 years ago

a4b0b48b

refactor(order/rel_iso): move statements about intervals to data/set/intervals (#8150)

eric-wieser committed 4 years ago

fb22ae33

chore(group_theory/perm/support): support_pow_le over nat (#8225)

pechersky committed 4 years ago

03e2cbd0

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

leanprover-community-bot committed 4 years ago

0ee238cf

feat(group_theory/perm/list): concrete permutations from a list (#7451)

pechersky committed 4 years ago

70aef28e

fix(data/complex/basic): ensure `algebra ℝ ℂ` is computable (#8166)

eric-wieser committed 4 years ago

5f2358c4

feat(algebra/group/units): teach `simps` about `units` (#8204)

eric-wieser committed 4 years ago

e0ca8534

fix(data/real/basic): provide a computable `module` instance (#8164)

eric-wieser committed 4 years ago

ce3d53b0

chore(feat/algebra/lie/from_cartan_matrix): rename file (#8219)

ocfnash committed 4 years ago

05e8ed24

docs(category_theory/limits/shapes/products): add module docstring (#8212)

b-mehta committed 4 years ago

836c5491

feat(data/fintype/list): induced fintype on nodup lists (#8171)

pechersky committed 4 years ago

51452619

chore(category_theory): homogenise usage of notation for terminal objects (#8106)

TwoFX committed 4 years ago

5796783b

chore(measure_theory/measure_space): add missing `finite_measure` instances (#8214)

kex-y committed 4 years ago

bb5ab1e7

feat(algebra/lie/from_cartan_matrix): construction of a Lie algebra from a Cartan matrix (#8206)

ocfnash committed 4 years ago

41ec92ea

feat(data/multiset/basic): add_eq_union_iff_disjoint (#8173)

pechersky committed 4 years ago

126a7b6e

feat(analysis/normed_space/int): norms of (units of) integers (#8136)

jcommelin committed 4 years ago

29beb1f3

fix(tactic/core): add subst' (#8129)

fpvandoorn committed 4 years ago

89e18376

feat(measure_theory/measure_space): if `f` restricted to `s` is measurable, then `f` is `ae_measurable` wrt `μ.restrict s` (#8098)

ADedecker committed 4 years ago

47c7c016

refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups (#8060)

adomani committed 4 years ago

06f0d517

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

leanprover-community-bot committed 4 years ago

20d8e837

chore(category_theory/monad/algebra): lint and golf (#8160)

b-mehta committed 4 years ago

d7653b8d

doc(data/set/function): add set. prefixes for doc-gen (#8215)

eric-wieser committed 4 years ago

03c8904a

doc(*): add bold in doc strings for named theorems i.e. **mean value theorem** (#8182)

hmonroe committed 4 years ago

ec07293a

feat(category_theory/closed): Exponential ideals (#4930)

b-mehta committed 4 years ago

13999970

feat(geometry/manifold/algebra): `left_invariant_derivation` (#8108)

Nicknamen committed 4 years ago

98e8408a

feat(category_theory/abelian/ext): Defines Ext functors. (#8186)

kim-em committed 4 years ago

23d22e4a

Older