leanprover-community/mathlib3

Pull Requests Commits

chore(linear_algebra/dimension): tidy lemma names for `linear_map.rank` (#18769)

eric-wieser committed 2 years ago

45ce3929

chore(linear_algebra/alternating,topology/algebra/module/multilinear): add a fun_like instance (#18766)

eric-wieser committed 2 years ago

284fdd29

feat(analysis/inner_product_space/symmetric): Polarization for `is_R_or_C` (#18397)

themathqueen committed 2 years ago

36172d66

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

github-actions[bot] committed 2 years ago

19cb3751

feat(linear_algebra/matrix/rank): generalize to rings (#18748)

eric-wieser committed 2 years ago

8535b76e

chore(category_theory): simps should not add hom lemmas (#18742)

kim-em committed 2 years ago

2efd2423

chore(linear_algebra/dimension): remove outdated comment (#18759)

eric-wieser committed 2 years ago

3a2039ad

chore(order/rel_iso/basic): better `namespace` management (#18758)

vihdzp committed 2 years ago

f29120f8

Apurva Nakade committed 2 years ago

66575dd2

Merge branch 'apurva/convex-cone-closure' into apurva/proper-cone

Apurva Nakade committed 2 years ago

d2183f63

better construction of closure

Apurva Nakade committed 2 years ago

9c1dfffb

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

MichaelStollBayreuth committed 2 years ago

dc65937e

simplify proof of smul_mem

apurvnakade committed 2 years ago

551fc5b6

add missing instance

apurvnakade committed 2 years ago

d5924e93

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)

github-actions[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)

github-actions[bot] committed 2 years ago

d64d67d0

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

alexjbest committed 2 years ago

3b1890e7

Newer Older