leanprover-community/mathlib

Pull Requests Commits

Merge branch 'CNF_golf' into CNF_alist'

vihdzp committed 2 years ago

10ed7753

revert simp inlines

vihdzp committed 2 years ago

7799c309

Update alist.lean

vihdzp committed 2 years ago

Verified bb593be6

Merge branch 'master' into CNF_alist'

vihdzp committed 2 years ago

d6179132

Merge branch 'CNF_golf' into CNF_alist'

vihdzp committed 2 years ago

64d70ca0

feat(number_theory/pell): add API for solutions (#18626)

MichaelStollBayreuth committed 2 years ago

dc65937e

chore(set_theory/cardinal/basic): missing lemmas about `<`/`≤` and `lift c`/`↑n` (#18752)

eric-wieser committed 2 years ago

9dba31df

feat(linear_algebra/finrank): generalize finrank to ring in more places (#18716)

eric-wieser committed 2 years ago

5ec62c81

chore(set_theory/cardinal/basic): missing lemmas about `lift c < ℵ₀` and `ℵ₀ < lift c` (#18746)

eric-wieser committed 2 years ago

e08a42b2

chore(linear_algebra/dimension): fix lemma names (#18747)

eric-wieser committed 2 years ago

67e606ea

feat(number_theory/number_field/canonical_embedding): add canonical embedding (#17783)

YaelDillies committed 2 years ago

60da01b4

chore(linear_algebra/dimension): deduplicate lemmas (#18743)

eric-wieser committed 2 years ago

5aa3c1de

chore(*): add mathlib4 synchronization comments (#18744)

leanprover-community-bot committed 2 years ago

75be6b61

feat(data/list/to_finsupp): computable finsupp from list (#15161)

pechersky committed 2 years ago

06a655b5

chore(linear_algebra/matrix/adjugate): add missing `matrix.of` wrapper (#18736)

eric-wieser committed 2 years ago

55102fc1

chore(category_theory/monad/basic): remove some simp lemmas (#18727)

kim-em committed 2 years ago

9c6816ca

refactor(linear_algebra/dimension): use `rank` in lemma names instead of `dim` (#18741)

eric-wieser committed 2 years ago

039a089d

feat(field_theory/is_alg_closed/algebraic_closure): add instances normal and is_galois for algebraic closure (#18730)

xroblot committed 2 years ago

0ac3057e

feat(analysis/schwartz_space): construction of continuous linear maps (#18651)

mcdoll committed 2 years ago

b2a5f0d6

feat(algebra/divisibility/basic): Dot notation aliases (#18698)

YaelDillies committed 2 years ago

e8638a0f

chore(*): add mathlib4 synchronization comments (#18726)

leanprover-community-bot committed 2 years ago

d64d67d0

chore(topology/algebra/group): generalise instances (#15171)

alexjbest committed 2 years ago

3b1890e7

feat(analysis/inner_product_space/basic): orthogonal submodules (#18705)

eric-wieser committed 2 years ago

1a4df69c

feat(analysis/calculus/iterated_deriv): equality of norms of iterated derivative (#18728)

mcdoll committed 2 years ago

d524d0a5

chore(linear_algebra/dimension): rename `rank` to `linear_map.rank` (#18734)

eric-wieser committed 2 years ago

be2ac64b

chore(linear_algebra/free_module/finite/rank): move lemmas from `module.free` to `finite_dimensional` (#18733)

eric-wieser committed 2 years ago

4cf7ca0e

chore(linear_algebra/finite_dimensional): generalize from Type to Sort (#18723)

eric-wieser committed 2 years ago

0ce07501

chore(linear_algebra/dimension): remove unecessary `nontrivial` argument (#18725)

eric-wieser committed 2 years ago

7aac545b

feat(measure_theory/function): Functions locally integrable on a set (#18673)

loefflerd committed 2 years ago

08a4542b

feat(algebra/group_power/lemmas): Induction principle for powers (#18668)

YaelDillies committed 2 years ago

e655e4ea

Older