leanprover-community/mathlib3

Pull Requests Commits

Make connection `matrix.has_one ↔ pi.single` explicit, golf

Vierkantor committed 4 years ago

292216d1

pechersky committed 4 years ago

7d0850d3

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib_aux

pechersky committed 4 years ago

282e3613

feat(topology/algebra/weak_dual_topology + analysis/normed_space/weak_dual_of_normed_space): add definition and first lemmas about weak-star topology (#8598)

kkytola committed 4 years ago

b7d980c5

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

leanprover-community-bot committed 4 years ago

ff721ad0

feat(data/real/ennreal): add `to_real_sub_of_le` (#8674)

kex-y committed 4 years ago

708d99aa

fix(tactic/norm_cast): assumption_mod_cast should only work on one goal (#8649)

robertylewis committed 4 years ago

46444478

chore(measure_theory): fix namespace in docstrings for docgen (#8671)

kex-y committed 4 years ago

c4208d22

feat(measure_theory/decomposition/jordan): the Jordan decomposition theorem for signed measures (#8645)

kex-y committed 4 years ago

8f863f6b

chore(data/option,data/set): a few lemmas, golf (#8636)

urkud committed 4 years ago

ba76bf75

feat(linear_algebra/basic) : add a small lemma for simplifying a map between equivalent quotient spaces (#8640)

Paul-Lez committed 4 years ago

721f571a

chore(data/(int, nat)/modeq): rationalize lemma names (#8644)

YaelDillies committed 4 years ago

c765b044

docs(data/int/basic): add module docstring (#8655)

YaelDillies committed 4 years ago

679a8a7c

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

leanprover-community-bot committed 4 years ago

36826cbe

feat(linear_algeba/linear_independent): coe_range (#8341)

kim-em committed 4 years ago

1b1088c2

feat(logic/basic): a few lemmas about `xor` (#8650)

urkud committed 4 years ago

50d3de92

feat(order/filter): change definition of inf (#8657)

PatrickMassot committed 4 years ago

94e4667b

feat(topology/*): lemmas about `dense`/`dense_range` and `is_(pre)connected` (#8651)

urkud committed 4 years ago

fdeb0646

fix(tactic/core): fix incorrect uses of with_ident_list (#8653)

digama0 committed 4 years ago

8b9c4cfc

feat(ring_theory): ideals in a Dedekind domain have unique factorization (#8530)

Vierkantor committed 4 years ago

7f5d5b9a

feat(field_theory): more general `algebra _ (algebraic_closure k)` instance (#8658)

Vierkantor committed 4 years ago

8eca2934

feat(linear_algebra/basic, group_theory/quotient_group, algebra/lie/quotient): ext lemmas for morphisms out of quotients (#8641)

eric-wieser committed 4 years ago

c711909c

feat(data/list/perm): subperm_ext_iff (#8504)

pechersky committed 4 years ago

9e83de22

chore(*): update lean to 3.32.1 (#8652)

digama0 committed 4 years ago

733e6e34

feat(finsupp/basic): restrict a finitely supported function on option A to A (#8342)

kim-em committed 4 years ago

03ddb8dd

feat(linear_algebra/invariant_basis_number): basic API lemmas (#7882)

kim-em committed 4 years ago

d0804bae

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

leanprover-community-bot committed 4 years ago

3b37614c

fix(tactic/core): mk_simp_attribute: remove superfluous disjunct (#8648)

digama0 committed 4 years ago

4a864ed0

feat(data/nat/(basic, modeq)): simple lemmas (#8647)

YaelDillies committed 4 years ago

ce26133b

refactor(tactic/*): mark internal attrs as `parser := failed` (#8635)

digama0 committed 4 years ago

c2580ebc

Older