leanprover-community/mathlib

Pull Requests Commits

Merge branch 'AD_lp_functorial' into AD_lp_curry

ADedecker committed 3 years ago

c9cbcff7

Better definition of `congr_right`

ADedecker committed 3 years ago

f28c79e5

ADedecker committed 3 years ago

11bbcb9d

Merge branch 'AD_lp_functorial' into AD_lp_curry

ADedecker committed 3 years ago

f9e84f27

ADedecker committed 3 years ago

4f4f6209

Finish renaming

ADedecker committed 3 years ago

9ff6e5a4

Update src/analysis/normed_space/lp_space.lean

ADedecker committed 3 years ago

Verified 4c25aeb0

Merge branch 'AD_injective_decidable_eq_protected' into AD_lp_functorial

ADedecker committed 3 years ago

c7f9f618

Make `function.injective.decidable_eq` protected

ADedecker committed 3 years ago

9af03251

ADedecker committed 3 years ago

8fab2bd5

refactor(algebra/homology): better defeqs, less case splitting (#15690)

jcommelin committed 3 years ago

13ff898b

ADedecker committed 3 years ago

53e99595

ADedecker committed 3 years ago

738aed0c

ADedecker committed 3 years ago

266ab572

ADedecker committed 3 years ago

2db919b2

fix(linear_algebra/prod): add missing `of_dual`s in lemma statements (#15750)

eric-wieser committed 3 years ago

cb3c2b9e

feat(field_theory/adjoin): A compositum of algebraic extensions is algebraic (#15724)

tb65536 committed 3 years ago

daac51e8

feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659)

tb65536 committed 3 years ago

7afd66ab

feat(algebra/direct_sum/decomposition): add an induction principle for `direct_sum.decomposition` class (#15654)

jjaassoonn committed 3 years ago

725ad273

feat(data/finset/pointwise): Singleton arithmetic (#15435)

YaelDillies committed 3 years ago

0fc357f5

feat(data/nat/factorization/basic): golf & move `card_multiples`, prove variant lemma `Ioc_filter_dvd_card_eq_div` (#15277)

stuart-presnell committed 3 years ago

87861dd7

docs(measure_theory/measure/haar): Mention uniqueness in module docstring (#15740)

rwbarton committed 3 years ago

df203bc8

docs(topology/sets/compacts): fix typo (#15739)

rwbarton committed 3 years ago

b7bde9df

feat(linear_algebra/matrix): inner prod of matrix (#14794)

abentkamp committed 3 years ago

1d0df917

feat(linear_algebra/clifford_algebra/even): Universal property and isomorphisms for the even subalgebra (#14790)

eric-wieser committed 3 years ago

56199b7b

refactor(linear_algebra, analysis/inner_product_space): use `⊤ ≤` instead of `= ⊤` in bases constructors (#15697)

ADedecker committed 3 years ago

6b647c3b

ADedecker committed 3 years ago

28290053

ADedecker committed 3 years ago

89a9ab9e

ADedecker committed 3 years ago

e7938ed6

feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)

ADedecker committed 3 years ago

4ff8c3db

Older