leanprover-community/mathlib

Pull Requests Commits

fix(linear_algebra/tensor_algebra): Correct the precedence of `⊗ₜ[R]` (#5619)

eric-wieser committed 5 years ago

d1b2d6eb

feat(scripts/lint-style.sh): check that Lean files don't have executable bit (#5606)

jcommelin committed 5 years ago

01e17a9d

feat(analysis/normed_space/inner_product): new versions of Cauchy-Schwarz equality case (#5586)

hrmacbeth committed 5 years ago

a6633e5b

refactor(measure_theory): integrate almost everywhere measurable functions (#5510)

sgouezel committed 5 years ago

1de608d8

chore(linear_algebra/alternating): Use `have` instead of `simp only` (#5618)

eric-wieser committed 5 years ago

8f9f5ca0

chore(scripts/*): rename files of the style linter (#5605)

jcommelin committed 5 years ago

78dc23ff

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

leanprover-community-bot committed 5 years ago

6dcfa5c2

feat(tactic/simps): some improvements (#5541)

fpvandoorn committed 5 years ago

12921e9e

feat(analysis/normed_space/{finite_dimension, inner_product}): assorted finite-dimensionality lemmas (#5580)

hrmacbeth committed 5 years ago

78d5bd37

feat(linear_algebra/alternating): Add comp_alternating_map and lemmas (#5476)

eric-wieser committed 5 years ago

7b825f2a

chore(computability/*FA): remove unnecessary type variables (#5613)

foxthomson committed 5 years ago

2300b477

feat(*): switch to lean 3.24 (#5612)

gebner committed 5 years ago

9535f914

chore(data/equiv/basic): Add refl / symm / trans lemmas for equiv_congr (#5609)

eric-wieser committed 5 years ago

7d0b9882

feat(data/set/basic): more lemmas about `set.pi` (#5603)

urkud committed 5 years ago

50beef25

feat(data/real/ennreal): add `ennreal.prod_lt_top` (#5602)

urkud committed 5 years ago

3669cb35

chore(logic/function): generalize `rel_update_iff` to `forall_update_iff` (#5601)

urkud committed 5 years ago

41501369

fix(data/nat/basic): fix typos in docstrings (#5592)

kbuzzard committed 5 years ago

6acf99e8

feat(data/*, order/*) supporting lemmas for characterising well-founded complete lattices (#5446)

Oliver Nash committed 5 years ago

afbf47d5

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

leanprover-community-bot committed 5 years ago

24340238

doc(overview): add dynamics and `measure.pi` (#5597)

urkud committed 5 years ago

1503cf89

fix(tactic/rcases): fix rcases? goal alignment (#5576)

digama0 committed 5 years ago

4fcf65c0

feat(measure_theory): almost everywhere measurable functions (#5568)

sgouezel committed 5 years ago

96948e45

feat(data/option/basic): join and associated lemmas (#5426)

pechersky committed 5 years ago

2967793e

feat(measure_theory/interval_integral): FTC-2 (#4945)

benjamindavidson committed 5 years ago

d04e034a

fix(algebra/module/basic): Do not attach the ℕ and ℤ `is_scalar_tower` and `smul_comm_class` instances to a specific definition of smul (#5509)

eric-wieser committed 5 years ago

46c35cc1

feat(measure_theory/lp_space): snorm is zero iff the function is zero ae (#5595)

RemyDegenne committed 5 years ago

e1138b00

feat(measure_theory/lp_space): add triangle inequality for the Lp seminorm (#5594)

RemyDegenne committed 5 years ago

ae2c8572

feat(computability/*FA): Deterministic and Nondeterministic Finite Automata (#5038)

foxthomson committed 5 years ago

384ba88b

feat(analysis/normed_space/basic): basic facts about the sphere (#5590)

hrmacbeth committed 5 years ago

eb6d5f15

feat(measure_theory/pi): finite products of measures (#5414)

fpvandoorn committed 5 years ago

0837fc30

Newer Older