leanprover-community/mathlib3

Pull Requests Commits

feat(field_theory/minimal_polynomial): add algebra_map_inj (#5062)

riccardobrasca committed 5 years ago

6f38a50d

fix(linear_algebra/multilinear): Fix incorrect type constraints on `dom_dom_congr` (#5203)

eric-wieser committed 5 years ago

986cabf3

chore(linear_algebra/determinant): Move some lemmas about swaps to better files (#5201)

eric-wieser committed 5 years ago

52697178

feat(group_theory/order_of_element): add is_cyclic_of_prime_card (#5172)

shingtaklam1324 committed 5 years ago

8ff9c0e6

Add `additive.sub_neg_monoid` / `multiplicative.div_inv_monoid`

Vierkantor committed 5 years ago

44d1dd53

Vierkantor committed 5 years ago

1cd41597

feat(algebra/module/basic): Add smul_comm_class instances (#5205)

eric-wieser committed 5 years ago

f1b387f8

feat(field_theory/separable): is_separable_of_alg_hom_is_separable (#5175)

tb65536 committed 5 years ago

a4b6c418

refactor(field_theory/fixed): Generalize alg_hom lemmas (#5174)

tb65536 committed 5 years ago

b978f366

feat(ring_theory/witt_vector/frobenius): the frobenius endomorphism of witt vectors (#4838)

jcommelin committed 5 years ago

e7c2bba1

Merge remote-tracking branch 'mathlib/master' into bundle_has_sub_div

Vierkantor committed 5 years ago

d00e6a81

feat(ring_theory/witt_vector): witt_sub, a demonstration of is_poly techniques (#5165)

jcommelin committed 5 years ago

f1531ea5

feat(group_theory/group_action/sub_mul_action): Add an object for bundled sets closed under a mul action (#4996)

eric-wieser committed 5 years ago

f6273d4d

feat(combinatorics/simple_graph/matching): introduce matchings and perfect matchings of graphs (#5156)

agusakov committed 5 years ago

98a20c25

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

leanprover-community-bot committed 5 years ago

61e76c42

chore(topology/algebra/ordered): add `order_iso.to_homeomorph` (#5111)

urkud committed 5 years ago

d9a7d05d

feat(category_theory/monad): mark monad lemmas as reassoc (#5190)

b-mehta committed 5 years ago

3f61e549

feat(category_theory/adjunction): adjunction to equivalence (#5189)

b-mehta committed 5 years ago

a84d7a71

feat(category_theory/adjunction): simp adjunction defs (#5188)

b-mehta committed 5 years ago

ed6eab01

feat(order/bounds): add basic lemmas about bdd_below (#5186)

ramonfmir committed 5 years ago

9be829e9

chore(data/polynomial/degree): golf some proofs, add simple lemmas (#5185)

urkud committed 5 years ago

e5befed7

feat(order/rel_iso): preimages of intervals under an `order_iso` (#5183)

urkud committed 5 years ago

64fd9f8c

feat(algebra/lie/basic): define `map` and `comap` for Lie ideals, submodules (#5181)

Oliver Nash committed 5 years ago

725fb8bc

feat(linear_algebra/multilinear): Generalize dom_dom_congr for equivalences between types (#5180)

eric-wieser committed 5 years ago

5e93545f

feat(data/set/function): Extend `update_comp` lemmas to work on dependent functions (#5178)

eric-wieser committed 5 years ago

8da5f23f

feat(data/option/basic): map_map functor-like lemmas (#5030)

pechersky committed 5 years ago

2189c7ab

feat(category_theory/limits): left adjoint if preserves colimits (#4942)

b-mehta committed 5 years ago

0bb88094

chore(analysis/normed_space): golf 2 proofs (#5184)

urkud committed 5 years ago

e5ea2000

feat(algebra/module/basic): generalize `is_scalar_tower` instances (#5135)

eric-wieser committed 5 years ago

a8ddd7b2

feat(linear_algebra/*): Use alternating maps for wedge and determinant (#5124)

eric-wieser committed 5 years ago

d6241cb0

Newer Older