leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/op_closed): make it easier to generalize over subobjects

eric-wieser committed 4 years ago

712e25bb

refactor(*): kill nat multiplication diamonds (#7084)

sgouezel committed 4 years ago

63801552

feat(data/finset/lattice): le_sup_iff and lt_sup_iff (#7182)

agjftucker committed 4 years ago

3ec54df5

feat(algebra/group/hom): `monoid_with_zero_hom.to_monoid_hom_injective` and co. (#7174)

benjamindavidson committed 4 years ago

500301e7

feat(algebraic_geometry): Basic opens form basis of zariski topology (#7152)

justus-springer committed 4 years ago

4d19f5fa

refactor(src/analysis/normed_space/linear_isometry): generalize to semi_normed_group (#7122)

riccardobrasca committed 4 years ago

724f804b

feat(src/set_theory/surreal): add numeric_add and numeric_omega lemmas (#7179)

apurvnakade committed 4 years ago

06f7d3f0

refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134)

adomani committed 4 years ago

46302c70

feat(logic/function/iterate): `f^[n]^[m] = f^[m]^[n]` (#7121)

adomani committed 4 years ago

92d5cab0

chore(data/equiv/basic): add simps attribute to some defs (#7137)

jcommelin committed 4 years ago

2af01474

feat(data/zsqrtd/basic): add coe_int_dvd_iff lemma (#7161)

Ruben-VandeVelde committed 4 years ago

a1c2bb7d

chore(data/matrix/basic): lemmas for `minor` about `diagonal`, `one`, and `mul` (#7133)

eric-wieser committed 4 years ago

16e2c6ca

refactor(algebra/big_operators, *): specialize `finset.prod_bij` to `fintype.prod_equiv` (#7109)

Vierkantor committed 4 years ago

f9c787da

feat(category_theory/subobject/factor_thru): lemmas in a preadditive category (#7104)

kim-em committed 4 years ago

001628b8

feat(finset/lattice): sup' is to sup as max' is to max (#7087)

agjftucker committed 4 years ago

68e894dc

feat(algebra/{algebra, module}/basic): make 3 smultiplication by 1 `simp` lemmas (#7166)

adomani committed 4 years ago

193dd5bb

feat(algebra/algebra/basic algebra/module/basic): add 3 lemmas m • (1 : R) = ↑m (#7094)

adomani committed 4 years ago

5694309f

feat(analysis/special_functions/exp_log): add `continuity` attribute to `continuous_exp` (#7157)

benjamindavidson committed 4 years ago

fbf62199

feat(measure_theory/interval_integral): variants of integral_comp lemmas (#7103)

benjamindavidson committed 4 years ago

1442f70a

feat(topology/continuous_function): comp_right_* (#7145)

kim-em committed 4 years ago

fc8e18c1

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

leanprover-community-bot committed 4 years ago

383f591e

feat(analysis/normed_space/finite_dimension): set of `f : E →L[𝕜] F` of rank `≥n` is open (#7022)

urkud committed 4 years ago

c6e62cfe

feat(linear_algebra/eigenspace): define the maximal generalized eigenspace (#7125)

ocfnash committed 4 years ago

a83230e0

feat(geometry/manifold): a manifold with σ-countable topology has second countable topology (#6948)

urkud committed 4 years ago

026150f3

chore(analysis/normed_space/inner_product): simplify two proofs (#7149)

bentoner committed 4 years ago

6b3803d6

chore(*): speedup slow proofs (#7148)

sgouezel committed 4 years ago

363a286b

feat(analysis/normed_space/banach): a range with closed complement is itself closed (#6972)

sgouezel committed 4 years ago

7e933678

feat(data/zsqrtd/basic): add some lemmas about norm (#7114)

Ruben-VandeVelde committed 4 years ago

d39c3a26

feat(group_theory/is_free_group): promote `is_free_group.lift'` to an equiv (#7110)

eric-wieser committed 4 years ago

7ae2af63

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

leanprover-community-bot committed 4 years ago

575b791e

Older