leanprover-community/mathlib3

Pull Requests Commits

chore(group_theory/subgroup): the range of a monoid/group/ring/module hom from a finite type is finite (#8293)

kbuzzard committed 4 years ago

468328da

feat(algebra/algebra/basic) new bit0/1_smul_one lemmas (#8394)

alexjbest committed 4 years ago

0bc800c2

chore(ring_theory): `set_like` instance for fractional ideals (#8275)

Vierkantor committed 4 years ago

7cdd7020

Merge branch 'monotone_interval_integrable' into integral_test

ADedecker committed 4 years ago

31aba502

A monotone function is interval_integrable

ADedecker committed 4 years ago

96f68572

chore(algebra/module/submodule): add submodule.coe_sum (#8393)

eric-wieser committed 4 years ago

38ac9ba7

chore(*): Prevent lemmas about the injectivity of `coe_fn` introducing un-reduced lambda terms (#8386)

eric-wieser committed 4 years ago

e2cda0bf

doc(algebra/to_additive): Add troubleshooting section (#8143)

fpvandoorn committed 4 years ago

54adb196

feat(group_theory/group_action): a monoid action determines a monoid hom (#8253)

dwarn committed 4 years ago

791d51c6

feat(algebra/lie/{submodule,subalgebra}): `lie_span`, `coe` form a Galois insertion (#8213)

ocfnash committed 4 years ago

6f88eeca

feat(algebra/lie/direct_sum): define `direct_sum.lie_of`, `direct_sum.to_lie_algebra`, `direct_sum.lie_algebra_is_internal` (#8369)

ocfnash committed 4 years ago

c9593dcc

feat(category_theory/limits): strict initial objects are initial mono (#8267)

b-mehta committed 4 years ago

df50b6c2

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

leanprover-community-bot committed 4 years ago

bc658188

fix(order/lattice, tactic.simps): add missing `notation_class` attributes to `has_(bot,top,inf,sup,compl)` (#8381)

eric-wieser committed 4 years ago

9e355305

feat(order): if `f x ≤ f y → x ≤ y`, then `f` is injective (#8373)

Vierkantor committed 4 years ago

f118c146

ADedecker committed 4 years ago

bbd87375

chore(topology/algebra/module): harmless generalization (#8389)

hrmacbeth committed 4 years ago

3e6c3675

Merge remote-tracking branch 'origin/master' into monotone_integrable

ADedecker committed 4 years ago

904e885a

ADedecker committed 4 years ago

004b9c5a

docs(analysis/normed_space/bounded_linear_map): add module docstring (#8263)

YaelDillies committed 4 years ago

ae1c7eef

feat(combinatorics/colex): order is decidable (#8378)

b-mehta committed 4 years ago

9fa82b05

Merge branch 'monotone_integrable' into integral_test

ADedecker committed 4 years ago

b5b0567c

feat(combinatorics/simple_graph): `boolean_algebra` for `simple_graph`s. (#8330)

ericrbg committed 4 years ago

28b85931

refactor(measure_theory/decomposition): move `decomposition` into a folder (#8374)

kex-y committed 4 years ago

fb58e059

feat(combinatorics/colex): top of the colex ordering on finite types (#8379)

b-mehta committed 4 years ago

b45acc9c

feat(analysis/normed_space): Define conformal maps on inner product spaces; define the groupoid of conformal maps (#8367)

justadzr committed 4 years ago

02a56964

feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375)

Vierkantor committed 4 years ago

899bb5f9

feat(data/sym2): add the universal property, and make `sym2.is_diag ⟦(x, y)⟧ ↔ x = y` true definitionally (#8358)

eric-wieser committed 4 years ago

4676b31f

feat(combinatorics/colex): golf and generalise (#8301)

b-mehta committed 4 years ago

6ac3059b

fix(data/matrix/basic): remove an accidental requirement for a matrix to be square (#8372)

l534zhan committed 4 years ago

ed8d597a

Newer Older