leanprover-community/mathlib

Pull Requests Commits

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

fix(*): Finish mul_assoc!

eric-wieser committed 5 years ago

c5f76577

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

JLimperg committed 5 years ago

69d41da5

feat(algebra/graded_algebra): Define a dependent version of add_monoid_algebra

eric-wieser committed 5 years ago

2ff209e8

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

feat(analysis/special_functions/trigonometric): simp attributes for trig values (#4806)

hrmacbeth committed 5 years ago

216cbc49

refactor(order/filter): make `filter.has_mem semireducible (#4807)

urkud committed 5 years ago

6dfa952c

chore(linear_algebra/affine_space/basic): split (#4767)

urkud committed 5 years ago

7807f3d3

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

leanprover-community-bot committed 5 years ago

4d1da548

feat(algebra/algebra/subalgebra): algebra equalizer (#4791)

tb65536 committed 5 years ago

c7379968

feat(data/vector2): scanl and associated lemmas (#4613)

pechersky committed 5 years ago

2a7e2158

chore(ring_theory/fractional_ideal): change exists_eq_span_singleton_mul (#4800)

faenuccio committed 5 years ago

51e12c00

refactor(data/polynomial): use `linear_map` for `monomial`, review `degree` (#4784)

riccardobrasca committed 5 years ago

97065dbf

feat(data/finset/lattice,order/basic): add lemmas in order_dual, prove dual order exchanges max' and min' (#4715)

adomani committed 5 years ago

a1ab984c

feat(data/vector2): add lemma map_id (#4799)

vaibhavkarve committed 5 years ago

1efbf13a

feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)` (#4782)

urkud committed 5 years ago

40e514cb

feat(category_theory/sites): pretopology (#4648)

b-mehta committed 5 years ago

99acfda0

feat(tactic/simps): user-provided names for projections (#4663)

fpvandoorn committed 5 years ago

a027a37b

refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762)

urkud committed 5 years ago

e0b153b2

Newer Older