leanprover-community/mathlib3

Pull Requests Commits

Try making `npow_rec` and `nsmul_rec` irreducible

Vierkantor committed 4 years ago

7dc0d02c

sgouezel committed 4 years ago

4b714c01

sgouezel committed 4 years ago

2d94f2fa

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

adomani committed 4 years ago

193dd5bb

fix refine_struct tests

kim-em committed 4 years ago

8bd4d850

fix equiv_rw tests

kim-em committed 4 years ago

90c25d7a

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

sgouezel committed 4 years ago

ec1532c2

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

sgouezel committed 4 years ago

d5cdc8b2

sgouezel committed 4 years ago

6e210f34

yet another speedup

sgouezel committed 4 years ago

9e07eb80

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

merge master, change definitions

sgouezel committed 4 years ago

734378f1

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

fix(refine_struct): fix regression from #2319

kim-em committed 4 years ago

a6444313

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

kim-em committed 4 years ago

309e3b08

Older