leanprover-community/mathlib

Pull Requests Commits

agusakov committed 4 years ago

6ab64a5d

yay we have definition

agusakov committed 4 years ago

da533768

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

feat(category_theory/action): currying (#7085)

dwarn committed 4 years ago

7138d354

feat(tactic/itauto): Complete intuitionistic prover (#7057)

digama0 committed 4 years ago

e269dbc1

feat(combinatorics/simple_graph/strongly_regular): add definition of strongly regular graph and proof that complete graph is SRG (#7044)

agusakov committed 4 years ago

8efb93b1

feat(category_theory/subobjects): improvements to API (#6932)

kim-em committed 4 years ago

309e3b08

chore(data/list/basic): avoid the axiom of choice (#7135)

eric-wieser committed 4 years ago

763c5c3a

Older