leanprover-community/mathlib

Pull Requests Commits

refactor(module/ordered): make ordered_semimodule a mixin (#4719)

kim-em committed 5 years ago

63c0dac6

feat(*): a, switch to lean 3.23 (#4802)

gebner committed 5 years ago

4003b3ee

Merge branch 'ordered_semimodule_mixin' into cauchy-rect

urkud committed 5 years ago

0e369835

Fix some lint errors

urkud committed 5 years ago

5a5ef654

Drop unneeded `{ .. }` trick

urkud committed 5 years ago

3a4bfef7

Merge branch 'master' into ordered_semimodule_mixin

urkud committed 5 years ago

f5290726

urkud committed 5 years ago

47e464fa

feat(analysis/asymptotics): Equivalent definitions for `is_[oO] u v l` looking like `u = φ * v` for some `φ` (#4646)

ADedecker committed 5 years ago

581b2af3

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

leanprover-community-bot committed 5 years ago

f510728a

Merge branch 'master' into cauchy-rect

urkud committed 5 years ago

9bb153ae

urkud committed 5 years ago

daa72402

feat(tactic/norm_num): make norm_num extensible (#4820)

digama0 committed 5 years ago

fc307f9b

feat(category_theory/sites): Grothendieck topology on a space (#4819)

b-mehta committed 5 years ago

2c7efdfc

feat(category_theory/limits/pullbacks): pullback self is id iff mono (#4813)

b-mehta committed 5 years ago

92af9fa8

feat(ring_theory/unique_factorization_domain): `unique_factorization_monoid` structure on polynomials over ufd (#4774)

awainverse committed 5 years ago

78811e0a

chore(data/equiv/basic): arrow_congr preserves properties of binary operators (#4759)

eric-wieser committed 5 years ago

856381c1

refactor(*): `midpoint`, `point_reflection`, and Mazur-Ulam in affine spaces (#4752)

urkud committed 5 years ago

ccc98d0a

feat(algebra/monoid_algebra): Add an equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` (#4402)

eric-wieser committed 5 years ago

4d19191e

feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

eric-wieser committed 5 years ago

d709ed6f

feat(category_theory/functor_category): monos in the functor category (#4811)

b-mehta committed 5 years ago

f83468d3

chore(category_theory/sites): nicer names (#4816)

b-mehta committed 5 years ago

7d7e850b

feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490)

eric-wieser committed 5 years ago

8b858d0b

feat(linear_algebra/finite_dimensional): finite dimensional algebra_hom of fields is bijective (#4793)

tb65536 committed 5 years ago

d510a637

feat(category_theory/Fintype): Adds the category of finite types and its "standard" skeleton. (#4809)

adamtopaz committed 5 years ago

1baf7017

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

leanprover-community-bot committed 5 years ago

d9c82152

feat(tactic/dependencies): add tactics to compute (reverse) dependencies (#4602)

JLimperg committed 5 years ago

69d41da5

feat(topology/algebra/group_with_zero): introduce `has_continuous_inv'` (#4804)

urkud committed 5 years ago

d75da1a2

chore(data/dfinsupp): Make some lemma arguments explicit (#4803)

eric-wieser committed 5 years ago

80ffad0c

feat(algebra/monoid_algebra): Bundle lift_nc_mul and lift_nc_one into a ring_hom and alg_hom (#4789)

eric-wieser committed 5 years ago

7a37dd4e

feat(ring_theory/unique_factorization_domain): a `normalization_monoid` structure for ufms (#4772)

awainverse committed 5 years ago

28cc74f8

Newer Older