leanprover-community/mathlib

Pull Requests Commits

Update rel_iso.lean

eric-wieser committed 4 years ago

Verified 2c814ece

Merge branch 'master' into eric-wieser/directed-monotone

eric-wieser committed 4 years ago

Verified f2ecb01a

feat(group_theory/submonoid): center of a submonoid (#8921)

eric-wieser committed 4 years ago

ab967d23

fix(order/rel_classes): remove looping instance (#8931)

fpvandoorn committed 4 years ago

6b63c034

fix(data/complex/basic): better formulas for nsmul and gsmul on complex to fix a diamond (#8928)

sgouezel committed 4 years ago

53f074ca

feat(logic/basic): equivalence of by_contra and choice (#8912)

digama0 committed 4 years ago

c04e8a48

feat(algebraic_geometry): Restriction of locally ringed spaces (#8809)

justus-springer committed 4 years ago

1c134548

refactor(order/atoms): reorder arguments of `is_simple_lattice.fintype` (#8933)

fpvandoorn committed 4 years ago

1dbd561f

feat(algebra/module/prod,pi): instances for actions with zero (#8929)

pechersky committed 4 years ago

22a297ca

chore(measure_theory/*): rename `probability_measure` and `finite_measure` (#8831)

hrmacbeth committed 4 years ago

f4d72050

feat(topology/algebra/ordered): monotone convergence in pi types (#8841)

urkud committed 4 years ago

6adb5e8b

chore(algebra/direct_sum/algebra): add missing rfl lemmas (#8924)

eric-wieser committed 4 years ago

4a65197a

fix(data/set/finite): drop {α : Type}, fixes universe issue (#8922)

jcommelin committed 4 years ago

aa0694a1

doc(tactic/lint): instructions on fails_quickly failure (#8910)

fpvandoorn committed 4 years ago

ad7519a3

chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)

urkud committed 4 years ago

b3807ee3

chore(algebra/monoid_algebra): convert a filename prefix into a folder (#8925)

eric-wieser committed 4 years ago

1e89df22

feat(algebra/direct_sum): graded algebras (#8783)

eric-wieser committed 4 years ago

98466d29

fix(ring_theory/polynomial/homogeneous): spelling mistake in `homogeneous` (#8914)

eric-wieser committed 4 years ago

2bae06af

feat(algebraic_geometry): Lift isomorphism of sheafed spaces to locally ringed spaces (#8887)

justus-springer committed 4 years ago

395bb6ca

refactor(data/set/finite): use `[fintype (plift ι)]` in `finite_Union` (#8872)

urkud committed 4 years ago

d75a2d96

feat(group_theory/perm/cycle_type): Fixed points of permutations of prime order (#8832)

tb65536 committed 4 years ago

db06b5a2

refactor(category_theory/limits/final): Symmetric API for final and initial functors (#8808)

justus-springer committed 4 years ago

e824b88d

chore(data/set_like): some additional documentation (#8765)

kmill committed 4 years ago

14a992b3

feat(group_theory/nilpotent): add subgroups of nilpotent group are nilpotent (#8854)

ineswright committed 4 years ago

0b485703

feat(measure_theory/decomposition/lebesgue): Lebesgue decomposition for sigma-finite measures (#8875)

kex-y committed 4 years ago

1aaff8da

feat(data/polynomial/basic): monomial_eq_zero_iff (#8897)

pechersky committed 4 years ago

42b5e801

feat(data/nat/log): Ceil log (#8764)

YaelDillies committed 4 years ago

8ee05e9a

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

leanprover-community-bot committed 4 years ago

d3c592f0

feat(data/real/irrational): exists irrational between any two distinct rationals and reals (#8753)

FrickHazard committed 4 years ago

0fd51b1c

feat(ring_theory): define integrally closed domains (#8893)

Vierkantor committed 4 years ago

2eaec057

Older