Commits leanprover-community/mathlib

feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)

eric-wieser committed 5 years ago

5ae192eb

chore(topology/basic): the set of cluster pts of a filter is a closed set (#4815)

urkud committed 5 years ago

d46d0c27

chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)

eric-wieser committed 5 years ago

072cfc55

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

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

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

feat(category_theory/limits/presheaf): free cocompletion (#4740)

b-mehta committed 5 years ago

25df2671

feat(archive/imo): formalize IMO 1981 problem Q3 (#4599)

lacker committed 5 years ago

dfa85b54

feat(equiv/basic): use @[simps] (#4652)

fpvandoorn committed 5 years ago

40da087f

feat(ring_theory/valuation): ring of integers (#4729)

kckennylau committed 5 years ago

e8f8de67